mem_ofCountableInter — Mathlib

English

For a given hl and h_mono, a set s belongs to Filter.ofCountableInter l hl h_mono if and only if s ∈ l.

Русский

Для заданных hl и h_mono множество s принадлежит Filter.ofCountableInter l hl h_mono тогда и только тогда, когда s ∈ l.

LaTeX

$$$s \\in Filter.ofCountableInter\\ l\\ hl\\ h_mono \\ \\Leftrightarrow \\ s \\in l$$$

Lean4

@[simp]
theorem mem_ofCountableInter {l : Set (Set α)} (hl : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S ∈ l)
    (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) {s : Set α} : s ∈ Filter.ofCountableInter l hl h_mono ↔ s ∈ l :=
  Iff.rfl

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