isConstant_coe_const

Mathlib.Order.Filter.Germ.Basic

URI: https://scilib.ai/kg/mathlib#Filter.Germ.isConstant_coe_const

English

The germ of the constant map is a constant germ.

Русский

Зародыш константной функции представляет собой константный зародыш.

LaTeX

$$$ (\lambda x : \alpha \to \beta) \, (\text{const } b) \, : \, \mathrm{Germ}(l, \beta) \text{ is constant}$$$

Lean4

@[simp]
theorem isConstant_coe_const {l : Filter α} {b : β} : (fun _ : α ↦ b : Germ l β).IsConstant := by use b

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

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

Разделы

Аффилиация

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