mem_inf_principal — Mathlib

English

For any f, s, t, membership of s in f ⊓ 𝓟 t is equivalent to membership of the set {x | x ∈ t → x ∈ s} in f.

Русский

Для любого фильтра f, подмножеств s и t: s ∈ f ⊓ 𝓟 t эквивалентно членству множества {x | x ∈ t → x ∈ s} в f.

LaTeX

$$$s \\in f \\sqcap \\mathcal{P}(t) \\iff \\{x \\mid x \\in t \\rightarrow x \\in s\\} \\in f$$$

Lean4

theorem mem_inf_principal {f : Filter α} {s t : Set α} : s ∈ f ⊓ 𝓟 t ↔ {x | x ∈ t → x ∈ s} ∈ f := by
  simp only [mem_inf_principal', imp_iff_not_or, setOf_or, compl_def, setOf_mem_eq]

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