coe_prod — Mathlib

English

The carrier of the product subsemiring s.prod t equals the cartesian product of the carriers: (s.prod t) : Set(R × S) = (s : Set R) × (t : Set S).

Русский

Множество-носитель произведения равен декартову произведению носителей: (s.prod t) : Set(R × S) = (s : Set R) × (t : Set S).

LaTeX

$$$ (s.prod t : Set(R \\times S)) = (s : Set R) \\times (t : Set S) $$$

Lean4

@[norm_cast]
theorem coe_prod (s : NonUnitalSubsemiring R) (t : NonUnitalSubsemiring S) :
    (s.prod t : Set (R × S)) = (s : Set R) ×ˢ (t : Set S) :=
  rfl

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