English
Same as 158127: if every x is bounded above by some element of s in a manner, atTop equals generated Ici'' s.
Русский
То же, что и в 158127: если для каждого x существует y из s, такой что x ≤ y, то atTop = generate(Ici'' s).
LaTeX
$$$\\forall x,\\exists y\\in s:\\ x\\le y \\Rightarrow (atTop) = generate(\\mathrm{Ici}'' s).$$$
Lean4
theorem atTop_eq_generate_of_forall_exists_le [Preorder α] {s : Set α} (hs : ∀ x, ∃ y ∈ s, x ≤ y) :
(atTop : Filter α) = generate (Ici '' s) :=
by
rw [atTop_eq_generate_Ici]
apply le_antisymm
· rw [le_generate_iff]
rintro - ⟨y, -, rfl⟩
exact mem_generate_of_mem ⟨y, rfl⟩
· rw [le_generate_iff]
rintro - ⟨x, -, -, rfl⟩
rcases hs x with ⟨y, ys, hy⟩
have A : Ici y ∈ generate (Ici '' s) := mem_generate_of_mem (mem_image_of_mem _ ys)
have B : Ici y ⊆ Ici x := Ici_subset_Ici.2 hy
exact sets_of_superset (generate (Ici '' s)) A B
