option_elim' — Mathlib

English

If a family f indexed by ι is locally finite, then the family obtained by replacing the value at None by a fixed set s is also locally finite. In symbols, LocallyFinite f ⇒ LocallyFinite (Option.elim' s f).

Русский

Если семейство f, индексируемое по ι, локально конечно, то и семейство, полученное заменой значения в None на фиксированное множество s, также локально конечно.

LaTeX

$$$\\operatorname{LocallyFinite}(f) \\Rightarrow \\operatorname{LocallyFinite}(\\operatorname{Option.elim}'s f)$$$

Lean4

theorem option_elim' (hf : LocallyFinite f) (s : Set X) : LocallyFinite (Option.elim' s f) :=
  locallyFinite_option.2 hf

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