mem_ofCountableUnion — Mathlib

English

A simp lemma identifying membership in the countable union filter with membership in the base filter via complement.

Русский

Простая лемма о принадлежности к фильтру счетного объединения через дополнение.

LaTeX

$$$s \\in Filter.ofCountableUnion l hunion hmono \\iff l(s^c)$$$

Lean4

@[simp]
theorem mem_ofCountableUnion {l : Set (Set α)} {hunion hmono s} : s ∈ ofCountableUnion l hunion hmono ↔ l sᶜ :=
  Iff.rfl

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