prod_range_range_eq — Mathlib

English

For functions f : α → β and g : α → γ, the set { (f x, g x) | x ∈ α } is contained in range(f) × range(g).

Русский

Множество пар (f(x), g(x)) для x ∈ α вложено в range(f) × range(g).

LaTeX

$$$ \{ (f x, g x) : x \in \alpha \} \subseteq \operatorname{range}(f) \timesˢ \operatorname{range}(g) $$$

Lean4

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

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