Mathlib.Data.Set.List

Set.range_list_map theorem

(f : α → β) : range (map f) = {l | ∀ x ∈ l, x ∈ range f}

Full source

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⟩

Range of List Mapping Equals Lists with Elements in Range of $f$

Informal description

For any function $f : \alpha \to \beta$, the range of the list mapping operation $\mathrm{map}\,f$ is equal to the set of all lists $l$ over $\beta$ such that every element $x$ in $l$ belongs to the range of $f$. That is, \[ \mathrm{range}(\mathrm{map}\,f) = \{l \mid \forall x \in l, x \in \mathrm{range}(f)\}. \]

Set.range_list_map_coe theorem

(s : Set α) : range (map ((↑) : s → α)) = {l | ∀ x ∈ l, x ∈ s}

Full source

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

Range of List Mapping via Inclusion Equals Lists with Elements in Subset

Informal description

For any subset $s$ of a type $\alpha$, the range of the list mapping operation applied to the canonical inclusion map $\uparrow : s \to \alpha$ is equal to the set of all lists $l$ over $\alpha$ such that every element $x$ in $l$ belongs to $s$. That is, \[ \mathrm{range}(\mathrm{map}\,(\uparrow)) = \{l \mid \forall x \in l, x \in s\}. \]

Set.range_list_get theorem

: range l.get = {x | x ∈ l}

Full source

@[simp]
theorem range_list_get : range l.get = { x | x ∈ l } := by
  ext x
  rw [mem_setOf_eq, mem_iff_get, mem_range]

Range of List Get Function Equals List Elements

Informal description

For any list `l`, the range of the function `l.get` (which retrieves elements by their index) is equal to the set of all elements in `l`, i.e., $\mathrm{range}(l.\mathrm{get}) = \{x \mid x \in l\}$.

Set.range_list_getElem? theorem

: range (l[·]? : ℕ → Option α) = insert none (some '' {x | x ∈ l})

Full source

theorem range_list_getElem? :
    range (l[·]? : ℕ → Option α) = insert none (somesome '' { x | x ∈ l }) := by
  rw [← range_list_get, ← range_comp]
  refine (range_subset_iff.2 fun n => ?_).antisymm (insert_subset_iff.2 ⟨?_, ?_⟩)
  · exact (le_or_lt l.length n).imp getElem?_eq_none_iff.mpr
      (fun hlt => ⟨⟨_, hlt⟩, (getElem?_eq_getElem hlt).symm⟩)
  · exact ⟨_, getElem?_eq_none_iff.mpr le_rfl⟩
  · exact range_subset_iff.2 fun k => ⟨_, getElem?_eq_getElem _⟩

Range of List Indexing Function Equals None Union Some of List Elements

Informal description

For any list `l` of elements of type `α`, the range of the function that retrieves elements by their index (returning an `Option α`) is equal to the set formed by inserting `none` into the image of the set $\{x \mid x \in l\}$ under the `some` constructor. That is, \[ \mathrm{range}(\lambda n, l[n]?) = \{\mathrm{none}\} \cup \{\mathrm{some}(x) \mid x \in l\}. \]

Set.range_list_getD theorem

(d : α) : (range fun n : Nat => l[n]?.getD d) = insert d {x | x ∈ l}

Full source

@[simp]
theorem range_list_getD (d : α) : (range fun n : Nat => l[n]?.getD d) = insert d { x | x ∈ l } :=
  calc
    (range fun n => l[n]?.getD d) = (fun o : Option α => o.getD d) '' range (l[·]?) := by
      simp only [← range_comp, Function.comp_def]
      rfl
    _ = insert d { x | x ∈ l } := by
      simp only [Option.getD, range_list_getElem?, image_insert_eq, image_image, image_id']

Range of List Indexing with Default Value: $\mathrm{range}(l[n]?.getD d) = \{d\} \cup \{x \mid x \in l\}$

Informal description

For any list `l` of elements of type `α` and a default value `d : α`, the range of the function that retrieves elements by their index (returning `d` when the index is out of bounds) is equal to the set formed by inserting `d` into the set of all elements in `l`. That is, \[ \mathrm{range}(\lambda n, l[n]?.getD d) = \{d\} \cup \{x \mid x \in l\}. \]

Set.range_list_getI theorem

[Inhabited α] (l : List α) : range l.getI = insert default {x | x ∈ l}

Full source

@[simp]
theorem range_list_getI [Inhabited α] (l : List α) :
    range l.getI = insert default { x | x ∈ l } := by
  unfold List.getI
  simp

Range of List Indexing with Default Value: $\mathrm{range}(l[\cdot]) = \{\mathrm{default}\} \cup \{x \mid x \in l\}$

Informal description

For any inhabited type $\alpha$ and list $l$ of elements of type $\alpha$, the range of the function that retrieves elements by their index (returning the default value when the index is out of bounds) is equal to the set formed by inserting the default value of $\alpha$ into the set of all elements in $l$. That is, \[ \mathrm{range}(l[\cdot]) = \{\mathrm{default}\} \cup \{x \mid x \in l\}. \]

List.canLift instance

(c) (p) [CanLift α β c p] : CanLift (List α) (List β) (List.map c) fun l => ∀ x ∈ l, p x

Full source

/-- If each element of a list can be lifted to some type, then the whole list can be
lifted to this type. -/
instance List.canLift (c) (p) [CanLift α β c p] :
    CanLift (List α) (List β) (List.map c) fun l => ∀ x ∈ l, p x where
  prf l H := by
    rw [← Set.mem_range, Set.range_list_map]
    exact fun a ha => CanLift.prf a (H a ha)

Lifting Condition for Lists

Informal description

For any types $\alpha$ and $\beta$ with a lifting condition specified by `CanLift α β c p`, where $c : \beta \to \alpha$ is the lifting function and $p : \alpha \to \text{Prop}$ is the condition, the list type `List α` can be lifted to `List β` via the function `List.map c`, provided that every element $x$ in the list satisfies $p(x)$. In other words, if every element of a list can be lifted from $\alpha$ to $\beta$ under condition $p$, then the entire list can be lifted to a list over $\beta$ using the mapping function $c$.