coe_prod — Mathlib · SciLib

English

The underlying set of the product LowerSet is the product of the underlying sets: ((s ×ˢ t : LowerSet (α × β)) : Set (α × β)) = (s : Set α) ×ˢ t.

Русский

Опорное множество произведения LowerSet равно произведению априорных множеств: подмножество как множество на (α×β) равно произведению подмножеств s и t.

LaTeX

$$$((s \times^{\mathrm{S}} t) : \mathrm{Set}(\alpha \times \beta)) = (s : \mathrm{Set}\,\alpha) \times^{\mathrm{S}} (t)$$$

Lean4

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

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