English
The atTop filter on Finset α equals the infimum over x of principal sets of ICI{x}.
Русский
Фильтр atTop на Finset α равен инфимуму по x от главных множеств ICI{x}.
LaTeX
$$$(\text{atTop} : \text{Filter}(\text{Finset } α)) = \bigwedge_{x:α} \mathcal{P}(\{y\in α : y \ge x\})$$$
Lean4
theorem atTop_finset_eq_iInf : (atTop : Filter (Finset α)) = ⨅ x : α, 𝓟 (Ici { x }) :=
by
refine le_antisymm (le_iInf fun i => le_principal_iff.2 <| mem_atTop ({ i } : Finset α)) ?_
refine le_iInf fun s => le_principal_iff.2 <| mem_iInf_of_iInter s.finite_toSet (fun i => mem_principal_self _) ?_
simp only [subset_def, mem_iInter, SetCoe.forall, mem_Ici, Finset.le_iff_subset, Finset.mem_singleton,
Finset.subset_iff, forall_eq]
exact fun t => id
