option_map — Mathlib

English

If f semiconjugates ga to gb, then Option.map f semiconjugates Option.map ga to Option.map gb.

Русский

Если f полуприводит ga к gb, то Option.map f полуприводит Option.map ga к Option.map gb.

LaTeX

$$$ \text{Semiconj}(Option.map f, Option.map ga, Option.map gb) $$$

Lean4

/-- If `f : α → β` semiconjugates `ga : α → α` to `gb : β → β`,
then `Option.map f` semiconjugates `Option.map ga` to `Option.map gb`. -/
theorem option_map {f : α → β} {ga : α → α} {gb : β → β} (h : Semiconj f ga gb) :
    Semiconj (Option.map f) (Option.map ga) (Option.map gb)
  | none => rfl
  | some _ => congr_arg some <| h _

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