English
For filters f1,f2 on α and g1,g2 on β, f1.coprod g1 ⊓ f2 × g2 ≤ f1 × g2 ⊔ f2 × g1.
Русский
Для фильтров f1,f2 на α и g1,g2 на β верно, что f1.coprod g1 ⊓ f2 × g2 ≤ f1 × g2 ⊔ f2 × g1.
LaTeX
$$$ f_1 \coprod g_1 \;\inf\; f_2 \times g_2 \;\le\; f_1 \times g_2 \;\sqcup\; f_2 \times g_1. $$$
Lean4
theorem coprod_inf_prod_le (f₁ f₂ : Filter α) (g₁ g₂ : Filter β) : f₁.coprod g₁ ⊓ f₂ ×ˢ g₂ ≤ f₁ ×ˢ g₂ ⊔ f₂ ×ˢ g₁ :=
calc
f₁.coprod g₁ ⊓ f₂ ×ˢ g₂
_ = (f₁ ×ˢ ⊤ ⊔ ⊤ ×ˢ g₁) ⊓ f₂ ×ˢ g₂ := by rw [coprod_eq_prod_top_sup_top_prod]
_ = f₁ ×ˢ ⊤ ⊓ f₂ ×ˢ g₂ ⊔ ⊤ ×ˢ g₁ ⊓ f₂ ×ˢ g₂ := (inf_sup_right _ _ _)
_ = (f₁ ⊓ f₂) ×ˢ g₂ ⊔ f₂ ×ˢ (g₁ ⊓ g₂) := by simp [prod_inf_prod]
_ ≤ f₁ ×ˢ g₂ ⊔ f₂ ×ˢ g₁ := sup_le_sup (prod_mono inf_le_left le_rfl) (prod_mono le_rfl inf_le_left)
