range_comp_subset_range

Mathlib.Data.Set.Image

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

English

range (g ∘ f) ⊆ range g.

Русский

Образ композиции g ∘ f ⊆ образ g.

LaTeX

$$$ \\operatorname{range}(g \\circ f) \\subseteq \\operatorname{range} g$$$

Lean4

theorem range_comp_subset_range (f : α → β) (g : β → γ) : range (g ∘ f) ⊆ range g := by grind

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

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

Разделы

Аффилиация

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