range_list_map_coe — Mathlib

English

A corollary of range_list_map: for a set s, the range of the coercion map from the subtype s to α is the same as the set of lists whose elements all lie in s.

Русский

Следствие из range_list_map: для множества s предел отображения из подтипа s в α равен множеству списков, элементы которых принадлежат s.

LaTeX

$$$\\text{range}(\\text{map} \\operatorname{Subtype.val}) = \\{l \\mid \\forall x \\in l, x \\in s\\}$$$

Lean4

theorem range_list_map_coe (s : Set α) : range (map ((↑) : s → α)) = {l | ∀ x ∈ l, x ∈ s} := by
  rw [range_list_map, Subtype.range_coe]

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