mem_atTop_sets — Mathlib

English

A set s belongs to atTop iff there exists an a such that every point b with b ≥ a lies in s.

Русский

Множество s принадлежит atTop тогда и только тогда, когда существует a, для которого все b ≥ a удовлетворяют b ∈ s.

LaTeX

$$$ s \\in (\\mathrm{atTop} : \\mathrm{Filter}\\, \\alpha) \\iff \\exists a : \\alpha, \\forall b \\ge a, b \\in s $$$

Lean4

@[simp]
theorem mem_atTop_sets {s : Set α} : s ∈ (atTop : Filter α) ↔ ∃ a : α, ∀ b ≥ a, b ∈ s :=
  atTop_basis.mem_iff.trans <| exists_congr fun _ => iff_of_eq (true_and _)

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