map_bot

Mathlib.Order.Hom.Basic

URI: https://scilib.ai/kg/mathlib#OrderIso.map_bot

English

Any order isomorphism preserves bottom: f ⊥ = ⊥.

Русский

Любой изоморфизм порядка сохраняет нижнюю границу: f(⊥) = ⊥.

LaTeX

$$$f: \alpha \simeq_o \beta \implies f(\bot_\alpha) = \bot_\beta$$$

Lean4

theorem map_bot [LE α] [PartialOrder β] [OrderBot α] [OrderBot β] (f : α ≃o β) : f ⊥ = ⊥ :=
  f.map_bot' (fun _ => bot_le) fun _ => bot_le

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

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

Разделы

Аффилиация

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