range_pair_subset

Mathlib.Data.Set.Prod

URI: https://scilib.ai/kg/mathlib#Set.range_pair_subset

English

Let 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 range_pair_subset (f : α → β) (g : α → γ) : (range fun x => (f x, g x)) ⊆ range f ×ˢ range g := by grind

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru