flatMap_mk — Mathlib

English

Applying flatMap via mk preserves structure: (ListBlank.mk l).flatMap f hf = ListBlank.mk (List.flatMap f l).

Русский

Применение flatMap через mk сохраняет структуру: (ListBlank.mk l).flatMap f hf = ListBlank.mk (List.flatMap f l).

LaTeX

$$$\forall {\Gamma} {\Gamma'} [Inhabited(\Gamma)] [Inhabited(\Gamma')] (l : List(\Gamma)) (f : \Gamma → List(\Gamma')) (hf) : (ListBlank.mk l).flatMap f hf = ListBlank.mk (List.flatMap f l)$$$

Lean4

@[simp]
theorem flatMap_mk {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (l : List Γ) (f : Γ → List Γ') (hf) :
    (ListBlank.mk l).flatMap f hf = ListBlank.mk (l.flatMap f) :=
  rfl

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