eventually_prod_principal_iff — Mathlib

English

For f : α → β × γ, b ∈ Filter β, c ∈ Filter γ, comap f (b ×ˢ c) equals the inf of comaps along the first and second projections: comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c.

Русский

Для отображения f: α → β×γ и фильтров b и c, комап образа равен пересечению предобразов по первым и вторым координатам.

LaTeX

$$$\\mathrm{comap}\\ f\\ (b \\timesˢ c) = \\mathrm{comap}(\\mathrm{Prod.fst} \\circ f)\\ b \\;\\sqcap\\; \\mathrm{comap}(\\mathrm{Prod.snd} \\circ f)\\ c$$$

Lean4

theorem eventually_prod_principal_iff {p : α × β → Prop} {s : Set β} :
    (∀ᶠ x : α × β in f ×ˢ 𝓟 s, p x) ↔ ∀ᶠ x : α in f, ∀ y : β, y ∈ s → p (x, y) :=
  by
  rw [eventually_iff, eventually_iff, mem_prod_principal]
  simp only [mem_setOf_eq]

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