atTop_eq — Mathlib

English

For any set s, if every x has some y ∈ s with x ≤ y, then atTop equals the generated filter of Ici'' s.

Русский

Для любого множества s, если для каждого x существует y ∈ s такое, что x ≤ y, то atTop равен сгенерированному фильтру от набора Ici'' s.

LaTeX

$$$\\forall x,\\exists y\\in s:\\ x\\le y\\ \\Rightarrow\\ (atTop: Filter\\ α) = generate(Ici'' s).$$$

Lean4

theorem _root_.IsTop.atTop_eq [Preorder α] {a : α} (ha : IsTop a) : atTop = 𝓟 (Ici a) :=
  (iInf_le _ _).antisymm <| le_iInf fun b ↦ principal_mono.2 <| Ici_subset_Ici.2 <| ha b

Похожие утверждения