mem_ofCardinalInter — Mathlib

English

For hc: 2 < c, hl, and h_mono, an s belongs to the constructed Filter.ofCardinalInter iff s ∈ l.

Русский

Пусть hc > 2, hl и h_mono; элемент s принадлежит построенному фильтру Filter.ofCardinalInter тогда и только тогда, когда s ∈ l.

LaTeX

$$$s \\in \\mathrm{Filter.ofCardinalInter}(l, hc, hl, h_mono) \\iff s \\in l$$$

Lean4

@[simp]
theorem mem_ofCardinalInter {l : Set (Set α)} (hc : 2 < c) (hl : ∀ S : Set (Set α), (#S < c) → S ⊆ l → ⋂₀ S ∈ l)
    (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) {s : Set α} : s ∈ Filter.ofCardinalInter l hc hl h_mono ↔ s ∈ l :=
  Iff.rfl

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