withTop

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#IsMin.withTop

English

If a is a minimal element of α, then its image in WithTop(α) is a minimal element as well.

Русский

Если a минимальный элемент α, то образ a в WithTop(α) также минимален.

LaTeX

$$$\text{IsMin}(a) \implies \text{IsMin}(a : \mathrm{WithTop}(\alpha))$$$

Lean4

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

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

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

Разделы

Аффилиация

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