FlatMap Singleton Cast Simplification

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.NewtonIdentities

Statement

Theorem FlatMap Singleton Cast Simplification
[blueprint]

$\mathrm{flatMap}\bigl(a \mapsto [(a : \mathbb{R})],\; l\bigr) = \mathrm{map}(\uparrow, l).$

theorem flatMap_singleton_cast (l : List ℕ) :
    List.flatMap (fun a => [(a : ℝ)]) l = l.map (↑) := by
Proof ▼ 


  induction l with
  | nil => rfl
  | cons h t ih =>
    change [(h : ℝ)] ++ List.flatMap (fun a => [(a : ℝ)]) t = (h : ℝ) :: t.map (↑)
    rw [ih]
    rfl

Dependencies (uses)

None

Dependents (used by)

None

Neighborhood

Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms