coe_inf

Mathlib.Topology.ContinuousMap.Ordered

URI: https://scilib.ai/kg/mathlib#ContinuousMap.coe_inf

English

The coercion commutes with inf: ↑(f ⊓ g) = ↑f ⊓ ↑g.

Русский

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

LaTeX

$$@[simp, norm_cast] (↑(f ⊓ g)) = ↑f ⊓ ↑g$$

Lean4

@[simp, norm_cast]
theorem coe_inf (f g : C(α, β)) : ⇑(f ⊓ g) = ⇑f ⊓ g :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru