mem_filter_prod_comm — Mathlib

English

Let α be a type and s ⊆ α × α be symmetric (IsSymmetricRel s). For any filters f and g on α, s belongs to the product filter f × g if and only if s belongs to the swapped product filter g × f.

Русский

Пусть α — множество, и s ⊆ α × α симметрично (IsSymmetricRel s). Для любых фильтров f и g на α выполняется: s ∈ f × g тогда и только тогда, когда s ∈ g × f.

LaTeX

$$$\\forall \\alpha\\,\\forall s\\subseteq \\alpha\\times \\alpha\\,\\bigl(\\mathrm{IsSymmetricRel}(s)\\Rightarrow \\forall f,g \\text{ фильтры на }\\alpha,\n\\; s\\in f\\times g \\iff s\\in g\\times f\\bigr)$$$

Lean4

theorem mem_filter_prod_comm {s : Set (α × α)} {f g : Filter α} (hs : IsSymmetricRel s) : s ∈ f ×ˢ g ↔ s ∈ g ×ˢ f := by
  rw [← hs.eq, ← mem_map, ← prod_comm, hs.eq]

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