prod_principal_principal — Mathlib

English

The product of two principal filters equals the principal of the product set: 𝓟 S ×ˢ 𝓟 T = 𝓟 (S ×ˢ T).

Русский

Произведение двух главных фильтров равно главному фильтру множества-результата: 𝓟 S ×ˢ 𝓟 T = 𝓟 (S ×ˢ T).

LaTeX

$$$ \\mathcal{P}S \\times\\! \\mathcal{P}T = \\mathcal{P}(S \\times\\! T) $$$

Lean4

@[simp]
theorem prod_principal_principal {s : Set α} {t : Set β} : 𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t) := by
  simp only [prod_eq_inf, comap_principal, principal_eq_iff_eq, comap_principal, inf_principal]; rfl

Похожие утверждения