Theorems · Theorem · general topology

Filter.prod_comap_comap_eq

∀ {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : β₁ → α₁}
  {m₂ : β₂ → α₂}, Filter.comap m₁ f₁ ×ˢ Filter.comap m₂ f₂ = Filter.comap (fun p => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂)

Defined in

Mathlib.Order.Filter.Prod

Cited by

5 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound