mem_atBot_sets — Mathlib

English

A set s belongs to atBot iff there exists a with ∀ b ≤ a, b ∈ s.

Русский

Множество s принадлежит atBot тогда и только тогда, когда существует a: ∀ b ≤ a, b ∈ s.

LaTeX

$$$ s \\in (\\mathrm{atBot} : \\mathrm{Filter}\\, α) \\iff \\exists a : α, \\forall b \\le a, b \\in s $$$

Lean4

@[simp]
theorem mem_atBot_sets {s : Set α} : s ∈ (atBot : Filter α) ↔ ∃ a : α, ∀ b ≤ a, b ∈ s :=
  mem_atTop_sets (α := αᵒᵈ)

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