range_enumerateCountable_of_mem — Mathlib

English

If s is countable with default ∈ s, then range(enumerateCountable h default) = s.

Русский

Если s счётно и default ∈ s, то range(enumerateCountable h default) = s.

LaTeX

$$$\operatorname{range}(\operatorname{enumerateCountable}(h,\text{default})) = s$$$

Lean4

theorem range_enumerateCountable_of_mem {s : Set α} (h : s.Countable) {default : α} (h_mem : default ∈ s) :
    range (enumerateCountable h default) = s :=
  subset_antisymm ((range_enumerateCountable_subset h _).trans_eq (insert_eq_of_mem h_mem))
    (subset_range_enumerate h default)

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