Theorems · Theorem · general topology

Filter.prod_lift_lift

∀ {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} {f₁ : Filter α₁} {f₂ : Filter α₂}
  {g₁ : Set α₁ → Filter β₁} {g₂ : Set α₂ → Filter β₂},
  Monotone g₁ → Monotone g₂ → f₁.lift g₁ ×ˢ f₂.lift g₂ = f₁.lift fun s => f₂.lift fun t => g₁ s ×ˢ g₂ t

Defined in

Mathlib.Order.Filter.Lift

Cited by

1 results in Mathlib

Foundations

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