diff_mem_iff — Mathlib

English

For any ultrafilter f and sets s,t, s \\ t ∈ f iff s ∈ f and t ∉ f.

Русский

Для любых ульрафильтров f и множеств s,t, s \ t ∈ f тогда и только тогда, когда s ∈ f и t ∉ f.

LaTeX

$$$\\\\forall {f \\\\in \\\\mathrm{Ultrafilter}(\\\\alpha)} {s t \\\\subseteq \\\\alpha}, s \\\\setminus t \in f \\\\Leftrightarrow (s \\\\in f) \\\\land (t \\\\notin f)$$$

Lean4

theorem diff_mem_iff (f : Ultrafilter α) : s \ t ∈ f ↔ s ∈ f ∧ t ∉ f :=
  inter_mem_iff.trans <| and_congr Iff.rfl compl_mem_iff_notMem

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