subsingleton_iff — Mathlib

English

If a filter l has a basis given by p and s, then l is subsingleton if and only if there exists an index i with p(i) true and s(i) is subsingleton.

Русский

Если у фильтра l есть основание вида p i, s i, то l является подсинглетным тогда и только тогда, когда существует индекс i с p(i) истинно и s(i) подсинглетно.

LaTeX

$$$$ l.HasBasis\ p\ s \Rightarrow (l.Subsingleton \iff \exists i, p i \land (s i).Subsingleton) $$$$

Lean4

theorem subsingleton_iff {ι : Sort*} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) :
    l.Subsingleton ↔ ∃ i, p i ∧ (s i).Subsingleton :=
  h.exists_iff fun _ _ hsub h ↦ h.anti hsub

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