coe_inf

Mathlib.Topology.ContinuousMap.Bounded.Normed

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

English

The infimum map is compatible with the coercions from f and g by coe_inf equality.

Русский

Неравенство инфимума согласуется с переходами по коинф.

LaTeX

$$$f \\inf g$ respects $\\mathrm{coe}$: $\\mathrm{coe}(f \\inf g)=\\mathrm{coe}(f) \\inf \\mathrm{coe}(g)$$$

Lean4

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

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

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

Разделы

Аффилиация

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