coe_prod — Mathlib

English

The carrier of the product upper set equals the product of the carriers.

Русский

Опорная подмножество произведения верхних множеств совпадает с произведением множеств.

LaTeX

$$((UpperSet.instSProd.sprod s t) : Set (α × β)) = (s : Set α) ×ˢ (t : Set β)$$

Lean4

@[simp, norm_cast]
theorem coe_prod : ((s ×ˢ t : UpperSet (α × β)) : Set (α × β)) = (s : Set α) ×ˢ t :=
  rfl

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