of_image

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#CovBy.of_image

English

If f is an OrderEmbedding and f a ⋖ f b, then a ⋖ b.

Русский

Если f — вложение порядка и f a ⋖ f b, тогда a ⋖ b.

LaTeX

$$$ (f a \\;⋖\\; f b) \\Rightarrow a \\,⋖\\, b $$$

Lean4

theorem of_image (f : α ↪o β) (h : f a ⋖ f b) : a ⋖ b :=
  ⟨f.lt_iff_lt.mp h.lt, fun _ hac hcb => h.2 (f.lt_iff_lt.mpr hac) (f.lt_iff_lt.mpr hcb)⟩

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

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

Разделы

Аффилиация

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