range_ite_subset'

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.range_ite_subset'

English

For any p, [Decidable], range (ite p f g) is a subset of range f ∪ range g.

Русский

Для любого p с разрешимостью, range (ite p f g) ⊆ range f ∪ range g.

LaTeX

$$$$ \\operatorname{range}(\\mathrm{ite}\\ p\\ f\\ g) \\subseteq \\operatorname{range}(f) \\cup \\operatorname{range}(g) $$$$

Lean4

theorem range_ite_subset' {p : Prop} [Decidable p] {f g : α → β} : range (if p then f else g) ⊆ range f ∪ range g := by
  grind

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

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

Разделы

Аффилиация

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