lookmap_map_eq — Mathlib

English

If g is constant on the images of f, i.e. ∀a, ∀ b ∈ f a, g a = g b, then map g (l.lookmap f) = map g l for all lists l.

Русский

Если g одинаково на изображениях f, то map g (l.lookmap f) = map g l для всех списков l.

LaTeX

$$$\\forall l:\\mathrm{List}\\ \\alpha,\\ map\\ g\\ (l.lookmap\\ f) = map\\ g\\ l \\text{ при условии }\\forall a,\\forall b \\in f\\ a,\\ g\\ a = g\\ b.$$$

Lean4

theorem lookmap_map_eq (g : α → β) (h : ∀ (a), ∀ b ∈ f a, g a = g b) : ∀ l : List α, map g (l.lookmap f) = map g l
  | [] => rfl
  | a :: l => by
    rcases h' : f a with - | b
    · simpa [h'] using lookmap_map_eq _ h l
    · simp [lookmap_cons_some _ _ h', h _ _ h']

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