English
If f1×g1 = f2×g2 then f1=f2 and g1=g2 (under NeBot).
Русский
Если произведения фильтров равны, то соответствующие компоненты равны (при условии NeBot).
LaTeX
$$$f_1 \times g_1 = f_2 \times g_2 \;\Rightarrow\; (f_1 = f_2) \land (g_1 = g_2)$ под условием NeBot$$
Lean4
@[simp]
theorem prod_inj {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} [NeBot f₁] [NeBot g₁] :
f₁ ×ˢ g₁ = f₂ ×ˢ g₂ ↔ f₁ = f₂ ∧ g₁ = g₂ :=
by
refine ⟨fun h => ?_, fun h => h.1 ▸ h.2 ▸ rfl⟩
have hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂ := prod_le_prod.1 h.le
haveI := neBot_of_le hle.1; haveI := neBot_of_le hle.2
exact ⟨hle.1.antisymm <| (prod_le_prod.1 h.ge).1, hle.2.antisymm <| (prod_le_prod.1 h.ge).2⟩
