coe_inf — Mathlib

English

The coercion of the infimum of two order-preserving maps equals the infimum of their coercions: (f ⊓ g) coerces to f ⊓ g pointwise.

Русский

Приведение к функциям сохраняет инфимум: (f ⊓ g) как функция равен f(a) ⊓ g(a).

LaTeX

$$$((f ⊓ g : α →o β) : α → β) = (f : α → β) ⊓ g$$$

Lean4

@[simp]
theorem coe_inf [SemilatticeInf β] (f g : α →o β) : ((f ⊓ g : α →o β) : α → β) = (f : α → β) ⊓ g :=
  rfl

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