[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
t t' : Bornology α
h_cobounded : cobounded α = cobounded α
⊢ t = t'
[PROOFSTEP]
cases t
[GOAL]
case mk
ι : Type u_1
α : Type u_2
β : Type u_3
t' : Bornology α
cobounded'✝ : Filter α
le_cofinite'✝ : cobounded'✝ ≤ cofinite
h_cobounded : cobounded α = cobounded α
⊢ { cobounded' := cobounded'✝, le_cofinite' := le_cofinite'✝ } = t'
[PROOFSTEP]
cases t'
[GOAL]
case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
cobounded'✝¹ : Filter α
le_cofinite'✝¹ : cobounded'✝¹ ≤ cofinite
cobounded'✝ : Filter α
le_cofinite'✝ : cobounded'✝ ≤ cofinite
h_cobounded : cobounded α = cobounded α
⊢ { cobounded' := cobounded'✝¹, le_cofinite' := le_cofinite'✝¹ } =
    { cobounded' := cobounded'✝, le_cofinite' := le_cofinite'✝ }
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
⊢ univ ∈ {s | sᶜ ∈ B}
[PROOFSTEP]
rwa [← compl_univ] at empty_mem 
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
x✝ y✝ : Set α
hx : x✝ ∈ {s | sᶜ ∈ B}
hy : y✝ ∈ {s | sᶜ ∈ B}
⊢ x✝ ∩ y✝ ∈ {s | sᶜ ∈ B}
[PROOFSTEP]
simpa [compl_inter] using union_mem _ hx _ hy
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
⊢ { sets := {s | sᶜ ∈ B}, univ_sets := (_ : univᶜ ∈ B),
      sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ {s | sᶜ ∈ B} → x ⊆ y → yᶜ ∈ B),
      inter_sets := (_ : ∀ {x y : Set α}, x ∈ {s | sᶜ ∈ B} → y ∈ {s | sᶜ ∈ B} → x ∩ y ∈ {s | sᶜ ∈ B}) } ≤
    cofinite
[PROOFSTEP]
rw [le_cofinite_iff_compl_singleton_mem]
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
⊢ ∀ (x : α),
    {x}ᶜ ∈
      { sets := {s | sᶜ ∈ B}, univ_sets := (_ : univᶜ ∈ B),
        sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ {s | sᶜ ∈ B} → x ⊆ y → yᶜ ∈ B),
        inter_sets := (_ : ∀ {x y : Set α}, x ∈ {s | sᶜ ∈ B} → y ∈ {s | sᶜ ∈ B} → x ∩ y ∈ {s | sᶜ ∈ B}) }
[PROOFSTEP]
intro x
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
x : α
⊢ {x}ᶜ ∈
    { sets := {s | sᶜ ∈ B}, univ_sets := (_ : univᶜ ∈ B),
      sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ {s | sᶜ ∈ B} → x ⊆ y → yᶜ ∈ B),
      inter_sets := (_ : ∀ {x y : Set α}, x ∈ {s | sᶜ ∈ B} → y ∈ {s | sᶜ ∈ B} → x ∩ y ∈ {s | sᶜ ∈ B}) }
[PROOFSTEP]
change { x }ᶜᶜ ∈ B
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
x : α
⊢ {x}ᶜᶜ ∈ B
[PROOFSTEP]
rw [compl_compl]
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
x : α
⊢ {x} ∈ B
[PROOFSTEP]
exact singleton_mem x
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
sUnion_univ : ⋃₀ B = univ
x : α
⊢ {x} ∈ B
[PROOFSTEP]
rw [sUnion_eq_univ_iff] at sUnion_univ 
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (a : α), ∃ b, b ∈ B ∧ a ∈ b
x : α
⊢ {x} ∈ B
[PROOFSTEP]
rcases sUnion_univ x with ⟨s, hs, hxs⟩
[GOAL]
case intro.intro
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (a : α), ∃ b, b ∈ B ∧ a ∈ b
x : α
s : Set α
hs : s ∈ B
hxs : x ∈ s
⊢ {x} ∈ B
[PROOFSTEP]
exact subset_mem s hs { x } (singleton_subset_iff.mpr hxs)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Bornology α
s t : Set α
x : α
⊢ IsBounded sᶜ ↔ IsCobounded s
[PROOFSTEP]
rw [isBounded_def, isCobounded_def, compl_compl]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Bornology α
s t : Set α
x : α
⊢ IsBounded ∅
[PROOFSTEP]
rw [isBounded_def, compl_empty]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Bornology α
s t : Set α
x : α
⊢ univ ∈ cobounded α
[PROOFSTEP]
exact univ_mem
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Bornology α
s t : Set α
x : α
⊢ IsBounded {x}
[PROOFSTEP]
rw [isBounded_def]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Bornology α
s t : Set α
x : α
⊢ {x}ᶜ ∈ cobounded α
[PROOFSTEP]
exact le_cofinite _ (finite_singleton x).compl_mem_cofinite
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Bornology α
s t : Set α
x : α
⊢ IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t
[PROOFSTEP]
simp only [← isCobounded_compl_iff, compl_union, isCobounded_inter]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Bornology α
s t : Set α
x : α
inst✝ : Bornology β
f : α → β
⊢ comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)
[PROOFSTEP]
refine'
  ⟨fun h s hs => _, fun h t ht =>
    ⟨(f '' tᶜ)ᶜ, h <| IsCobounded.compl ht, compl_subset_comm.1 <| subset_preimage_image _ _⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Bornology α
s✝ t : Set α
x : α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
⊢ IsBounded (f '' s)
[PROOFSTEP]
obtain ⟨t, ht, hts⟩ := h hs.compl
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Bornology α
s✝ t✝ : Set α
x : α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : f ⁻¹' t ⊆ sᶜ
⊢ IsBounded (f '' s)
[PROOFSTEP]
rw [subset_compl_comm, ← preimage_compl] at hts 
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Bornology α
s✝ t✝ : Set α
x : α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : s ⊆ f ⁻¹' tᶜ
⊢ IsBounded (f '' s)
[PROOFSTEP]
exact (IsCobounded.compl ht).subset ((image_subset f hts).trans <| image_preimage_subset _ _)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
t t' : Bornology α
h : ∀ (s : Set α), IsBounded s ↔ IsBounded s
⊢ t = t'
[PROOFSTEP]
ext s
[GOAL]
case h_cobounded.a
ι : Type u_1
α : Type u_2
β : Type u_3
t t' : Bornology α
h : ∀ (s : Set α), IsBounded s ↔ IsBounded s
s : Set α
⊢ s ∈ cobounded α ↔ s ∈ cobounded α
[PROOFSTEP]
simpa [@isBounded_def _ t, isBounded_def, compl_compl] using h sᶜ
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
s : Set α
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (x : α), {x} ∈ B
⊢ IsBounded s ↔ s ∈ B
[PROOFSTEP]
rw [@isBounded_def _ (ofBounded B empty_mem subset_mem union_mem sUnion_univ), ← Filter.mem_sets,
  ofBounded_cobounded_sets, Set.mem_setOf_eq, compl_compl]
  -- porting note: again had to use `@isBounded_def _` and feed Lean the instance
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
s✝ : Set α
inst✝ : Bornology α
s : Set ι
f : ι → Set α
hs : Set.Finite s
⊢ IsBounded (⋃ (i : ι) (_ : i ∈ s), f i) ↔ ∀ (i : ι), i ∈ s → IsBounded (f i)
[PROOFSTEP]
simp only [← isCobounded_compl_iff, compl_iUnion, isCobounded_biInter hs]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
s : Set α
inst✝ : Bornology α
S : Set (Set α)
hs : Set.Finite S
⊢ IsBounded (⋃₀ S) ↔ ∀ (s : Set α), s ∈ S → IsBounded s
[PROOFSTEP]
rw [sUnion_eq_biUnion, isBounded_biUnion hs]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
s✝ : Set α
inst✝¹ : Bornology α
inst✝ : Finite ι
s : ι → Set α
⊢ IsBounded (⋃ (i : ι), s i) ↔ ∀ (i : ι), IsBounded (s i)
[PROOFSTEP]
rw [← sUnion_range, isBounded_sUnion (finite_range s), forall_range_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Bornology α
⊢ cobounded α = ⊥ ↔ BoundedSpace α
[PROOFSTEP]
rw [← isBounded_univ, isBounded_def, compl_univ, empty_mem_iff_bot]
