prod_principal — Mathlib

English

If la has basis pa sa and sb is a fixed set with a basis, then la ×ˢ 𝓟(sb) has basis pa with basic sets sa ×ˢ sb.

Русский

Если у la есть базис pa sa, а у sb — фиксированное множество с базисом, то произведение la ×ˢ 𝓟(sb) имеет базис pa с базисными множствами sa ×ˢ sb.

LaTeX

$$$(la \times\mathcal{P}(sb)) HasBasis pa (sa \times sb ·).$$

Lean4

protected theorem prod_principal (h : la.HasBasis pa sa) (sb : Set β) : (la ×ˢ 𝓟 sb).HasBasis pa (sa · ×ˢ sb) := by
  simpa only [prod_eq_inf, comap_principal, prod_eq] using (h.comap Prod.fst).inf_principal _

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