English
Finite index pi-space: if each coordinate satisfies a_i < x_i < b_i, then Icc(a,b) is a neighborhood of x.
Русский
Для конечного индекса, если a_i < x_i < b_i, то Icc(a,b) близко к x.
LaTeX
$$Icc a b ∈ 𝓝 x under ∀ i, a_i < x_i and ∀ i, x_i < b_i$$
Lean4
instance instIsCountablyGenerated_atTop [OrderTopology α] [SecondCountableTopology α] :
IsCountablyGenerated (atTop : Filter α) :=
by
by_cases h : ∃ (x : α), IsTop x
· rcases h with ⟨x, hx⟩
rw [atTop_eq_pure_of_isTop hx]
exact isCountablyGenerated_pure x
· rcases exists_countable_basis α with ⟨b, b_count, b_ne, hb⟩
have : Countable b := by exact Iff.mpr countable_coe_iff b_count
have A : ∀ (s : b), ∃ (x : α), x ∈ (s : Set α) := by
intro s
have : (s : Set α) ≠ ∅ := by
intro H
apply b_ne
convert s.2
exact H.symm
exact Iff.mp notMem_singleton_empty this
choose a ha using A
have : (atTop : Filter α) = (generate (Ici '' (range a))) :=
by
apply atTop_eq_generate_of_not_bddAbove
intro ⟨x, hx⟩
simp only [IsTop, not_exists, not_forall, not_le] at h
rcases h x with ⟨y, hy⟩
obtain ⟨s, sb, -, hs⟩ : ∃ s, s ∈ b ∧ y ∈ s ∧ s ⊆ Ioi x := hb.exists_subset_of_mem_open hy isOpen_Ioi
have I : a ⟨s, sb⟩ ≤ x := hx (mem_range_self _)
have J : x < a ⟨s, sb⟩ := hs (ha ⟨s, sb⟩)
exact lt_irrefl _ (I.trans_lt J)
rw [this]
exact ⟨_, (countable_range _).image _, rfl⟩
