finite_range_ite — Mathlib

English

If the ranges of f and g are finite and p is decidable, then the range of the piecewise function x ↦ if p x then f x else g x is finite.

Русский

Если диапазоны функций f и g конечны и p разрешимо, то диапазон функции x ↦ если p(x) то f(x) иначе g(x) конечен.

LaTeX

$$$ (\\operatorname{range}\\bigl(x \\mapsto \\operatorname{ite}(p x)\\, f x\\, g x\\bigr)).Finite $$$

Lean4

theorem finite_range_ite {p : α → Prop} [DecidablePred p] {f g : α → β} (hf : (range f).Finite)
    (hg : (range g).Finite) : (range fun x => if p x then f x else g x).Finite :=
  (hf.union hg).subset range_ite_subset

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