apply_covBy_apply_iff

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#Set.OrdConnected.apply_covBy_apply_iff

English

The pair (WCovBy, CovBy) forms a nonstrict-strict order on α.

Русский

Пара (WCovBy, CovBy) образует ненасыщенный строгий порядок на α.

LaTeX

$$$ IsNonstrictStrictOrder\\, α\\, (\\,⋖\\,): (WCovBy, CovBy) $$$

Lean4

theorem apply_covBy_apply_iff (f : α ↪o β) (h : (range f).OrdConnected) : f a ⋖ f b ↔ a ⋖ b :=
  ⟨CovBy.of_image f, fun hab => hab.image f h⟩

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

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

Разделы

Аффилиация

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