swap_covBy_swap

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#Prod.swap_covBy_swap

English

CovBy is preserved under swapping coordinates: CovBy(x.swap,y.swap) iff CovBy(x,y).

Русский

CovBy сохраняется при перестановке координат: CovBy(x.swap,y.swap) если и только если CovBy(x,y).

LaTeX

$$$ CovBy(x.swap,y.swap) \iff CovBy(x,y) $$$

Lean4

@[simp]
theorem swap_covBy_swap : x.swap ⋖ y.swap ↔ x ⋖ y :=
  apply_covBy_apply_iff (OrderIso.prodComm : α × β ≃o β × α)

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

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

Разделы

Аффилиация

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