English
For every function f : α → β, the range of List.map f equals the set of lists l such that every element x of l lies in range f.
Русский
Для любой функции f : α → β, область значений List.map f равна множеству списков l, для каждого элемента x из l выполняется x ∈ range f.
LaTeX
$$$\\text{range}(\\text{List.map } f) = \\{l \\mid \\forall x \\in l, x \\in \\text{range}(f)\\}$$$
Lean4
theorem range_list_map (f : α → β) : range (map f) = {l | ∀ x ∈ l, x ∈ range f} :=
by
refine antisymm (range_subset_iff.2 fun l => forall_mem_map.2 fun y _ => mem_range_self _) fun l hl => ?_
induction l with
| nil => exact ⟨[], rfl⟩
| cons a l ihl =>
rcases ihl fun x hx => hl x <| subset_cons_self _ _ hx with ⟨l, rfl⟩
rcases hl a mem_cons_self with ⟨a, rfl⟩
exact ⟨a :: l, map_cons⟩
