prod_range_univ_eq — Mathlib

English

The product of the whole set for the first coordinate 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 \big( \lambda p : \alpha \times \beta, (p.1, m_2 p.2) \big) $$$

Lean4

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

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