range_enumerateCountable_subset — Mathlib

English

The range of enumerateCountable h default is contained in insert default s.

Русский

Диапазон enumerateCountable ограничен вставкой по умолчанию в s.

LaTeX

$$$\mathrm{range}(\operatorname{enumerateCountable}(h,default)) \subseteq \operatorname{insert}(default, s)$$$

Lean4

theorem range_enumerateCountable_subset {s : Set α} (h : s.Countable) (default : α) :
    range (enumerateCountable h default) ⊆ insert default s :=
  by
  refine range_subset_iff.mpr (fun n ↦ ?_)
  rw [enumerateCountable]
  match @decode s (Countable.toEncodable h) n with
  | none => exact mem_insert _ _
  | some val => simp

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