prod_univ_range_eq — Mathlib

English

The product of the universal set on α and the range of m2 equals the range of the map p ↦ (p.1, m2 p.2).

Русский

Произведение всеобщего множества по α и диапазон m2 равно образу отображения p ↦ (p.1, m2 p.2).

LaTeX

$$$ (univ : Set\alpha) \timesˢ range m_2 = range fun p : \alpha \times \beta => (p.1, m_2 p.2) $$$

Lean4

theorem prod_univ_range_eq {m₂ : β → δ} : (univ : Set α) ×ˢ range m₂ = range fun p : α × β => (p.1, m₂ p.2) :=
  ext <| by simp [range]

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