English
If g1 and g2 are monotone, then the product of lifts equals the lift of the product: f1.lift g1 ×ˢ f2.lift g2 = f1.lift (s ↦ f2.lift (t ↦ g1 s ×ˢ g2 t)).
Русский
Если g1 и g2 монотонны, то произведение подъёмов равно подъему произведения: f1.lift g1 ×ˢ f2.lift g2 = f1.lift (s ↦ f2.lift (t ↦ g1 s ×ˢ g2 t)).
LaTeX
$$$f_1.lift g_1 \\timesˢ f_2.lift g_2 = f_1.lift (\\lambda s. f_2.lift (\\lambda t. g_1 s \\timesˢ g_2 t))$$$
Lean4
theorem prod_lift_lift {f₁ : Filter α₁} {f₂ : Filter α₂} {g₁ : Set α₁ → Filter β₁} {g₂ : Set α₂ → Filter β₂}
(hg₁ : Monotone g₁) (hg₂ : Monotone g₂) :
f₁.lift g₁ ×ˢ f₂.lift g₂ = f₁.lift fun s => f₂.lift fun t => g₁ s ×ˢ g₂ t :=
by
simp only [prod_def, lift_assoc hg₁]
apply congr_arg; funext x
rw [lift_comm]
apply congr_arg; funext y
apply lift'_lift_assoc hg₂
