withBotMap — Mathlib

English

Lift an order homomorphism f: α →o β to an order homomorphism WithBot α →o WithBot β by sending x to f x.

Русский

Поднять отображение а_й→β до отображения WithBot α →o WithBot β через x ↦ f x.

LaTeX

$$$\\text{withBotMap}(f):\\mathrm{WithBot}\\alpha \\too \\mathrm{WithBot}\\beta$$$

Lean4

/-- Lift an order homomorphism `f : α →o β` to an order homomorphism `WithBot α →o WithBot β`. -/
@[simps -fullyApplied]
protected def withBotMap (f : α →o β) : WithBot α →o WithBot β :=
  ⟨WithBot.map f, f.mono.withBot_map⟩

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