English
Under monotonicity of g1 and g2, the product of lift' filters equals the lift of the product: f1.lift' g1 ×ˢ f2.lift' g2 = f1.lift (λ s ⇒ f2.lift' (λ t ⇒ g1 s ×ˢ g2 t)).
Русский
При монотонности g1 и g2 произведение lift' фильтров равно подъему от произведения: 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 α₁ → Set β₁} {g₂ : Set α₂ → Set β₂}
(hg₁ : Monotone g₁) (hg₂ : Monotone g₂) :
f₁.lift' g₁ ×ˢ f₂.lift' g₂ = f₁.lift fun s => f₂.lift' fun t => g₁ s ×ˢ g₂ t :=
calc
f₁.lift' g₁ ×ˢ f₂.lift' g₂ = f₁.lift fun s => f₂.lift fun t => 𝓟 (g₁ s) ×ˢ 𝓟 (g₂ t) :=
prod_lift_lift (monotone_principal.comp hg₁) (monotone_principal.comp hg₂)
_ = f₁.lift fun s => f₂.lift fun t => 𝓟 (g₁ s ×ˢ g₂ t) := by { simp only [prod_principal_principal]
}
