withTopWithBot_apply — Mathlib

English

For f : LatticeHom α β and a : WithTop (WithBot α), the value of f.withTopWithBot at a is a.map (WithBot.map f).

Русский

Для f : LatticeHom α β и a : WithTop (WithBot α) значение f.withTopWithBot в a равно a.map (WithBot.map f).

LaTeX

$$$ f.withTopWithBot\\, a = a.\\mathrm{map}(\\mathrm{WithBot.map} \\; f) $$$

Lean4

theorem withTopWithBot_apply (f : LatticeHom α β) (a : WithTop <| WithBot α) :
    f.withTopWithBot a = a.map (WithBot.map f) :=
  rfl

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