withBot

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#IsMax.withBot

English

If a is maximal in α, then its image in WithBot α is maximal in WithBot α.

Русский

Если a максимален в α, то его образ в WithBot α максимален в WithBot α.

LaTeX

$$$ IsMax(a) \rightarrow IsMax(\iota(a)) $$$

Lean4

protected theorem _root_.IsMax.withBot (h : IsMax a) : IsMax (a : WithBot α) := fun x ↦ by cases x <;> simp;
  simpa using @h _

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

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

Разделы

Аффилиация

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