mem_inf_principal' — Mathlib

English

For any f, s, t, membership of s in f ⊓ 𝓟 t is equivalent to membership of t^c ∪ s in f.

Русский

Для произвольного фильтра f, подмножества s и t: s ∈ f ⊓ 𝓟 t эквивалентно (t^c ∪ s) ∈ f.

LaTeX

$$$s \\in f \\sqcap \\mathcal{P}(t) \\iff t^{c} \\cup s \\in f$$$

Lean4

theorem mem_inf_principal' {f : Filter α} {s t : Set α} : s ∈ f ⊓ 𝓟 t ↔ tᶜ ∪ s ∈ f := by
  simp only [← le_principal_iff, (isCompl_principal s).le_left_iff, disjoint_assoc, inf_principal,
    ← (isCompl_principal (t ∩ sᶜ)).le_right_iff, compl_inter, compl_compl]

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