range_ite_subset — Mathlib

English

For any p : α → Prop with DecidablePred p, range (fun x => ite (p x) (f x) (g x)) ⊆ range f ∪ range g.

Русский

Для любого p : α → Prop с DecidablePred, range (fun x => if p x then f x else g x) ⊆ range f ∪ range g.

LaTeX

$$$$ \\operatorname{range}(\\lambda x.\\, \\operatorname{ite}(p\\,x)\\; (f\\,x)\\; (g\\,x)) \\subseteq \\operatorname{range}(f) \\cup \\operatorname{range}(g) $$$$

Lean4

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

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