case a
α : Type u
β : Type v
γ : Type ?u.18094
δ : Type ?u.18097
ε : Type ?u.18100
ζ : Type ?u.18103
a : CofiniteTopology α
U : Set (CofiniteTopology α)
⊢ U ∈ 𝓝 a ↔ U ∈ pure a ⊔ cofinite
α : Type u
β : Type v
γ : Type ?u.18094
δ : Type ?u.18097
ε : Type ?u.18100
ζ : Type ?u.18103
a : CofiniteTopology α
⊢ 𝓝 a = pure a ⊔ cofinite
ext U
case a
α : Type u
β : Type v
γ : Type ?u.18094
δ : Type ?u.18097
ε : Type ?u.18100
ζ : Type ?u.18103
a : CofiniteTopology α
U : Set (CofiniteTopology α)
⊢ (∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t) ↔ U ∈ pure a ⊔ cofinite
case a
α : Type u
β : Type v
γ : Type ?u.18094
δ : Type ?u.18097
ε : Type ?u.18100
ζ : Type ?u.18103
a : CofiniteTopology α
U : Set (CofiniteTopology α)
⊢ U ∈ 𝓝 a ↔ U ∈ pure a ⊔ cofinite
rw [mem_nhds_iff]
case a.mp
α : Type u
β : Type v
γ : Type ?u.18094
δ : Type ?u.18097
ε : Type ?u.18100
ζ : Type ?u.18103
a : CofiniteTopology α
U : Set (CofiniteTopology α)
⊢ (∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t) → U ∈ pure a ⊔ cofinite

case a.mpr
α : Type u
β : Type v
γ : Type ?u.18094
δ : Type ?u.18097
ε : Type ?u.18100
ζ : Type ?u.18103
a : CofiniteTopology α
U : Set (CofiniteTopology α)
⊢ U ∈ pure a ⊔ cofinite → ∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t
case a
α : Type u
β : Type v
γ : Type ?u.18094
δ : Type ?u.18097
ε : Type ?u.18100
ζ : Type ?u.18103
a : CofiniteTopology α
U : Set (CofiniteTopology α)
⊢ (∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t) ↔ U ∈ pure a ⊔ cofinite
constructor
case a.mp.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.18094
δ : Type ?u.18097
ε : Type ?u.18100
ζ : Type ?u.18103
a : CofiniteTopology α
U V : Set (CofiniteTopology α)
hVU : V ⊆ U
V_op : IsOpen V
haV : a ∈ V
⊢ U ∈ pure a ⊔ cofinite
case a.mp
α : Type u
β : Type v
γ : Type ?u.18094
δ : Type ?u.18097
ε : Type ?u.18100
ζ : Type ?u.18103
a : CofiniteTopology α
U : Set (CofiniteTopology α)
⊢ (∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t) → U ∈ pure a ⊔ cofinite
rintro ⟨V, hVU, V_op, haV⟩
no goals
case a.mp.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.18094
δ : Type ?u.18097
ε : Type ?u.18100
ζ : Type ?u.18103
a : CofiniteTopology α
U V : Set (CofiniteTopology α)
hVU : V ⊆ U
V_op : IsOpen V
haV : a ∈ V
⊢ U ∈ pure a ⊔ cofinite
exact mem_sup.mpr ⟨hVU haV, mem_of_superset (V_op ⟨_, haV⟩) hVU⟩
case a.mpr.intro
α : Type u
β : Type v
γ : Type ?u.18094
δ : Type ?u.18097
ε : Type ?u.18100
ζ : Type ?u.18103
a : CofiniteTopology α
U : Set (CofiniteTopology α)
hU : a ∈ U
hU' : Set.Finite (Uᶜ)
⊢ ∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t
case a.mpr
α : Type u
β : Type v
γ : Type ?u.18094
δ : Type ?u.18097
ε : Type ?u.18100
ζ : Type ?u.18103
a : CofiniteTopology α
U : Set (CofiniteTopology α)
⊢ U ∈ pure a ⊔ cofinite → ∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t
rintro ⟨hU : a ∈ U, hU' : Uᶜ.Finite⟩
no goals
case a.mpr.intro
α : Type u
β : Type v
γ : Type ?u.18094
δ : Type ?u.18097
ε : Type ?u.18100
ζ : Type ?u.18103
a : CofiniteTopology α
U : Set (CofiniteTopology α)
hU : a ∈ U
hU' : Set.Finite (Uᶜ)
⊢ ∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t
exact ⟨U, Subset.rfl, fun _ => hU', hU⟩