X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
⊢ ↑F ≤ 𝓝 x → str X F = x
X : Compactum
F : Ultrafilter X.A
x : X.A
⊢ ↑F ≤ 𝓝 x → str X F = x
let fsu := Finset (Set (Ultrafilter X))
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
⊢ ↑F ≤ 𝓝 x → str X F = x
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
⊢ ↑F ≤ 𝓝 x → str X F = x
let ssu := Set (Set (Ultrafilter X))
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
⊢ ↑F ≤ 𝓝 x → str X F = x
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
⊢ ↑F ≤ 𝓝 x → str X F = x
let ι : fsu → ssu := fun x ↦ ↑x
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
⊢ ↑F ≤ 𝓝 x → str X F = x
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
⊢ ↑F ≤ 𝓝 x → str X F = x
let T0 : ssu := { S | ∃ A ∈ F, S = basic A }
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
⊢ ↑F ≤ 𝓝 x → str X F = x
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
⊢ ↑F ≤ 𝓝 x → str X F = x
let AA := X.str ⁻¹' {x}
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
⊢ ↑F ≤ 𝓝 x → str X F = x
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
⊢ ↑F ≤ 𝓝 x → str X F = x
let T1 := insert AA T0
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
⊢ ↑F ≤ 𝓝 x → str X F = x
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
⊢ ↑F ≤ 𝓝 x → str X F = x
let T2 := finiteInterClosure T1
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
⊢ str X F = x
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
⊢ ↑F ≤ 𝓝 x → str X F = x
intro cond
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
⊢ str X F = x
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
⊢ str X F = x
have claim1 : ∀ A : Set X, IsClosed A → A ∈ F → x ∈ A := by
  intro A hA h
  by_contra H
  rw [le_nhds_iff] at cond
  specialize cond (Aᶜ) H hA.isOpen_compl
  rw [Ultrafilter.mem_coe, Ultrafilter.compl_mem_iff_not_mem] at cond
  contradiction
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
⊢ str X F = x
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
⊢ str X F = x
have claim2 : ∀ A : Set X, A ∈ F → x ∈ cl A := by
  intro A hA
  exact claim1 (cl A) (isClosed_cl A) (mem_of_superset hA (subset_cl A))
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
⊢ str X F = x
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
⊢ str X F = x
have claim3 : ∀ (S1) (_ : S1 ∈ T0) (S2) (_ : S2 ∈ T0), S1 ∩ S2 ∈ T0 := by
  rintro S1 ⟨S1, hS1, rfl⟩ S2 ⟨S2, hS2, rfl⟩
  exact ⟨S1 ∩ S2, inter_mem hS1 hS2, by simp [basic_inter]⟩
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
⊢ str X F = x
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
⊢ str X F = x
have claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty := by
  rintro S ⟨S, hS, rfl⟩
  rcases claim2 _ hS with ⟨G, hG, hG2⟩
  exact ⟨G, hG2, hG⟩
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
⊢ str X F = x
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
⊢ str X F = x
have claim5 : ∀ S ∈ T0, Set.Nonempty S := by
  rintro S ⟨S, hS, rfl⟩
  exact ⟨F, hS⟩
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
⊢ ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
⊢ str X F = x
suffices ∀ F : fsu, ↑F ⊆ T1 → (⋂₀ ι F).Nonempty by
  obtain ⟨G, h1⟩ := Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty _ this
  have c1 : X.join G = F := Ultrafilter.coe_le_coe.1 fun P hP => h1 (Or.inr ⟨P, hP, rfl⟩)
  have c2 : G.map X.str = X.incl x := by
    refine' Ultrafilter.coe_le_coe.1 fun P hP => _
    apply mem_of_superset (h1 (Or.inl rfl))
    rintro x ⟨rfl⟩
    exact hP
  simp [← c1, c2]
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
T : fsu
hT : ↑T ⊆ T1
⊢ Set.Nonempty (⋂₀ ι T)
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
⊢ ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
intro T hT
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
T : fsu
hT : ↑T ⊆ T1
⊢ ↑T ⊆ finiteInterClosure T1
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
T : fsu
hT : ↑T ⊆ T1
⊢ Set.Nonempty (⋂₀ ι T)
refine' claim6 _ (finiteInter_mem (.finiteInterClosure_finiteInter _) _ _)
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
T : fsu
hT : ↑T ⊆ T1
t : Set (Ultrafilter X.A)
ht : t ∈ ↑T
⊢ t ∈ finiteInterClosure T1
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
T : fsu
hT : ↑T ⊆ T1
⊢ ↑T ⊆ finiteInterClosure T1
intro t ht
no goals
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
T : fsu
hT : ↑T ⊆ T1
t : Set (Ultrafilter X.A)
ht : t ∈ ↑T
⊢ t ∈ finiteInterClosure T1
exact finiteInterClosure.basic (@hT t ht)
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
A : Set X.A
hA : IsClosed A
h : A ∈ F
⊢ x ∈ A
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
⊢ ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
intro A hA h
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
A : Set X.A
hA : IsClosed A
h : A ∈ F
H : ¬x ∈ A
⊢ False
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
A : Set X.A
hA : IsClosed A
h : A ∈ F
⊢ x ∈ A
by_contra H
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ∀ (s : Set X.A), x ∈ s → IsOpen s → s ∈ ↑F
A : Set X.A
hA : IsClosed A
h : A ∈ F
H : ¬x ∈ A
⊢ False
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
A : Set X.A
hA : IsClosed A
h : A ∈ F
H : ¬x ∈ A
⊢ False
rw [le_nhds_iff] at cond
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
A : Set X.A
hA : IsClosed A
h : A ∈ F
H : ¬x ∈ A
cond : Aᶜ ∈ ↑F
⊢ False
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ∀ (s : Set X.A), x ∈ s → IsOpen s → s ∈ ↑F
A : Set X.A
hA : IsClosed A
h : A ∈ F
H : ¬x ∈ A
⊢ False
specialize cond (Aᶜ) H hA.isOpen_compl
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
A : Set X.A
hA : IsClosed A
h : A ∈ F
H : ¬x ∈ A
cond : ¬A ∈ F
⊢ False
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
A : Set X.A
hA : IsClosed A
h : A ∈ F
H : ¬x ∈ A
cond : Aᶜ ∈ ↑F
⊢ False
rw [Ultrafilter.mem_coe, Ultrafilter.compl_mem_iff_not_mem] at cond
no goals
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
A : Set X.A
hA : IsClosed A
h : A ∈ F
H : ¬x ∈ A
cond : ¬A ∈ F
⊢ False
contradiction
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
A : Set X.A
hA : A ∈ F
⊢ x ∈ Compactum.cl A
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
⊢ ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
intro A hA
no goals
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
A : Set X.A
hA : A ∈ F
⊢ x ∈ Compactum.cl A
exact claim1 (cl A) (isClosed_cl A) (mem_of_superset hA (subset_cl A))
case intro.intro.intro.intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
S1 : Set X.A
hS1 : S1 ∈ F
S2 : Set X.A
hS2 : S2 ∈ F
⊢ Compactum.basic S1 ∩ Compactum.basic S2 ∈ T0
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
⊢ ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
rintro S1 ⟨S1, hS1, rfl⟩ S2 ⟨S2, hS2, rfl⟩
no goals
case intro.intro.intro.intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
S1 : Set X.A
hS1 : S1 ∈ F
S2 : Set X.A
hS2 : S2 ∈ F
⊢ Compactum.basic S1 ∩ Compactum.basic S2 ∈ T0
exact ⟨S1 ∩ S2, inter_mem hS1 hS2, by simp [basic_inter]⟩
no goals
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
S1 : Set X.A
hS1 : S1 ∈ F
S2 : Set X.A
hS2 : S2 ∈ F
⊢ Compactum.basic S1 ∩ Compactum.basic S2 = Compactum.basic (S1 ∩ S2)
simp [basic_inter]
case intro.intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
S : Set X.A
hS : S ∈ F
⊢ Set.Nonempty (AA ∩ Compactum.basic S)
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
⊢ ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
rintro S ⟨S, hS, rfl⟩
case intro.intro.intro.intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
S : Set X.A
hS : S ∈ F
G : Ultrafilter X.A
hG : G ∈ Compactum.basic S
hG2 : str X G = x
⊢ Set.Nonempty (AA ∩ Compactum.basic S)
case intro.intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
S : Set X.A
hS : S ∈ F
⊢ Set.Nonempty (AA ∩ Compactum.basic S)
rcases claim2 _ hS with ⟨G, hG, hG2⟩
no goals
case intro.intro.intro.intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
S : Set X.A
hS : S ∈ F
G : Ultrafilter X.A
hG : G ∈ Compactum.basic S
hG2 : str X G = x
⊢ Set.Nonempty (AA ∩ Compactum.basic S)
exact ⟨G, hG2, hG⟩
case intro.intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
S : Set X.A
hS : S ∈ F
⊢ Set.Nonempty (Compactum.basic S)
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
⊢ ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
rintro S ⟨S, hS, rfl⟩
no goals
case intro.intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
S : Set X.A
hS : S ∈ F
⊢ Set.Nonempty (Compactum.basic S)
exact ⟨F, hS⟩
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ S ∈ T0 ∨ ∃ Q, Q ∈ T0 ∧ S = AA ∩ Q
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
⊢ ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → S ∈ T0 ∨ ∃ Q, Q ∈ T0 ∧ S = AA ∩ Q
intro S hS
case cond
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ FiniteInter T0

case H
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ S ∈ finiteInterClosure (insert AA T0)
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ S ∈ T0 ∨ ∃ Q, Q ∈ T0 ∧ S = AA ∩ Q
apply finiteInterClosure_insert
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
this : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → S ∈ T0 ∨ ∃ Q, Q ∈ T0 ∧ S = AA ∩ Q
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ Set.Nonempty S
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
this : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → S ∈ T0 ∨ ∃ Q, Q ∈ T0 ∧ S = AA ∩ Q
⊢ ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
intro S hS
case inl
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
this : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → S ∈ T0 ∨ ∃ Q, Q ∈ T0 ∧ S = AA ∩ Q
S : Set (Ultrafilter X.A)
hS : S ∈ T2
h : S ∈ T0
⊢ Set.Nonempty S

case inr
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
this : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → S ∈ T0 ∨ ∃ Q, Q ∈ T0 ∧ S = AA ∩ Q
S : Set (Ultrafilter X.A)
hS : S ∈ T2
h : ∃ Q, Q ∈ T0 ∧ S = AA ∩ Q
⊢ Set.Nonempty S
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
this : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → S ∈ T0 ∨ ∃ Q, Q ∈ T0 ∧ S = AA ∩ Q
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ Set.Nonempty S
cases' this _ hS with h h
no goals
case inl
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
this : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → S ∈ T0 ∨ ∃ Q, Q ∈ T0 ∧ S = AA ∩ Q
S : Set (Ultrafilter X.A)
hS : S ∈ T2
h : S ∈ T0
⊢ Set.Nonempty S
exact claim5 S h
case inr.intro.intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
this : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → S ∈ T0 ∨ ∃ Q, Q ∈ T0 ∧ S = AA ∩ Q
Q : Set (Ultrafilter X.A)
hQ : Q ∈ T0
hS : AA ∩ Q ∈ T2
⊢ Set.Nonempty (AA ∩ Q)
case inr
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
this : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → S ∈ T0 ∨ ∃ Q, Q ∈ T0 ∧ S = AA ∩ Q
S : Set (Ultrafilter X.A)
hS : S ∈ T2
h : ∃ Q, Q ∈ T0 ∧ S = AA ∩ Q
⊢ Set.Nonempty S
rcases h with ⟨Q, hQ, rfl⟩
no goals
case inr.intro.intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
this : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → S ∈ T0 ∨ ∃ Q, Q ∈ T0 ∧ S = AA ∩ Q
Q : Set (Ultrafilter X.A)
hQ : Q ∈ T0
hS : AA ∩ Q ∈ T2
⊢ Set.Nonempty (AA ∩ Q)
exact claim4 Q hQ
case cond.univ_mem
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ Set.univ ∈ T0

case cond.inter_mem
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ ∀ ⦃s : Set (Ultrafilter X.A)⦄, s ∈ T0 → ∀ ⦃t : Set (Ultrafilter X.A)⦄, t ∈ T0 → s ∩ t ∈ T0
case cond
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ FiniteInter T0
constructor
case cond.univ_mem
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ Set.univ ∈ F ∧ Set.univ = Compactum.basic Set.univ
case cond.univ_mem
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ Set.univ ∈ T0
use Set.univ
case cond.univ_mem
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ Set.univ = Compactum.basic Set.univ
case cond.univ_mem
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ Set.univ ∈ F ∧ Set.univ = Compactum.basic Set.univ
refine' ⟨Filter.univ_sets _, _⟩
case cond.univ_mem.h
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
x✝ : Ultrafilter X.A
⊢ x✝ ∈ Set.univ ↔ x✝ ∈ Compactum.basic Set.univ
case cond.univ_mem
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ Set.univ = Compactum.basic Set.univ
ext
case cond.univ_mem.h
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
x✝ : Ultrafilter X.A
⊢ x✝ ∈ Set.univ → x✝ ∈ Compactum.basic Set.univ
case cond.univ_mem.h
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
x✝ : Ultrafilter X.A
⊢ x✝ ∈ Set.univ ↔ x✝ ∈ Compactum.basic Set.univ
refine' ⟨_, by tauto⟩
no goals
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
x✝ : Ultrafilter X.A
⊢ x✝ ∈ Compactum.basic Set.univ → x✝ ∈ Set.univ
tauto
case cond.univ_mem.h
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
x✝ : Ultrafilter X.A
a✝ : x✝ ∈ Set.univ
⊢ x✝ ∈ Compactum.basic Set.univ
case cond.univ_mem.h
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
x✝ : Ultrafilter X.A
⊢ x✝ ∈ Set.univ → x✝ ∈ Compactum.basic Set.univ
intro
no goals
case cond.univ_mem.h
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
x✝ : Ultrafilter X.A
a✝ : x✝ ∈ Set.univ
⊢ x✝ ∈ Compactum.basic Set.univ
apply Filter.univ_sets
no goals
case cond.inter_mem
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ ∀ ⦃s : Set (Ultrafilter X.A)⦄, s ∈ T0 → ∀ ⦃t : Set (Ultrafilter X.A)⦄, t ∈ T0 → s ∩ t ∈ T0
exact claim3
no goals
case H
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ S ∈ finiteInterClosure (insert AA T0)
exact hS
case intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
this : ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ G.sets
⊢ str X F = x
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
this : ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
⊢ str X F = x
obtain ⟨G, h1⟩ := Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty _ this
case intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
this : ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ G.sets
c1 : join X G = F
⊢ str X F = x
case intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
this : ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ G.sets
⊢ str X F = x
have c1 : X.join G = F := Ultrafilter.coe_le_coe.1 fun P hP => h1 (Or.inr ⟨P, hP, rfl⟩)
case intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
this : ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ G.sets
c1 : join X G = F
c2 : Ultrafilter.map (str X) G = incl X x
⊢ str X F = x
case intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
this : ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ G.sets
c1 : join X G = F
⊢ str X F = x
have c2 : G.map X.str = X.incl x := by
  refine' Ultrafilter.coe_le_coe.1 fun P hP => _
  apply mem_of_superset (h1 (Or.inl rfl))
  rintro x ⟨rfl⟩
  exact hP
no goals
case intro
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
this : ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ G.sets
c1 : join X G = F
c2 : Ultrafilter.map (str X) G = incl X x
⊢ str X F = x
simp [← c1, c2]
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
this : ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ G.sets
c1 : join X G = F
P : Set X.A
hP : P ∈ ↑(incl X x)
⊢ P ∈ ↑(Ultrafilter.map (str X) G)
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
this : ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ G.sets
c1 : join X G = F
⊢ Ultrafilter.map (str X) G = incl X x
refine' Ultrafilter.coe_le_coe.1 fun P hP => _
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
this : ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ G.sets
c1 : join X G = F
P : Set X.A
hP : P ∈ ↑(incl X x)
⊢ AA ⊆ str X ⁻¹' P
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
this : ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ G.sets
c1 : join X G = F
P : Set X.A
hP : P ∈ ↑(incl X x)
⊢ P ∈ ↑(Ultrafilter.map (str X) G)
apply mem_of_superset (h1 (Or.inl rfl))
case refl
X : Compactum
F : Ultrafilter X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
G : Ultrafilter (Ultrafilter X.A)
c1 : join X G = F
P : Set X.A
x : Ultrafilter X.A
AA : Set (Ultrafilter X.A) := str X ⁻¹' {str X x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 (str X x)
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → str X x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → str X x ∈ Compactum.cl A
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
this : ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
h1 : T1 ⊆ G.sets
hP : P ∈ ↑(incl X (str X x))
⊢ x ∈ str X ⁻¹' P
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := str X ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → x ∈ Compactum.cl A
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
this : ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ G.sets
c1 : join X G = F
P : Set X.A
hP : P ∈ ↑(incl X x)
⊢ AA ⊆ str X ⁻¹' P
rintro x ⟨rfl⟩
no goals
case refl
X : Compactum
F : Ultrafilter X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
T0 : ssu := {S | ∃ A, A ∈ F ∧ S = Compactum.basic A}
claim3 : ∀ (S1 : Set (Ultrafilter X.A)), S1 ∈ T0 → ∀ (S2 : Set (Ultrafilter X.A)), S2 ∈ T0 → S1 ∩ S2 ∈ T0
claim5 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty S
G : Ultrafilter (Ultrafilter X.A)
c1 : join X G = F
P : Set X.A
x : Ultrafilter X.A
AA : Set (Ultrafilter X.A) := str X ⁻¹' {str X x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 (str X x)
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → str X x ∈ A
claim2 : ∀ (A : Set X.A), A ∈ F → str X x ∈ Compactum.cl A
claim4 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T0 → Set.Nonempty (AA ∩ S)
claim6 : ∀ (S : Set (Ultrafilter X.A)), S ∈ T2 → Set.Nonempty S
this : ∀ (F : fsu), ↑F ⊆ T1 → Set.Nonempty (⋂₀ ι F)
h1 : T1 ⊆ G.sets
hP : P ∈ ↑(incl X (str X x))
⊢ x ∈ str X ⁻¹' P
exact hP