swap_wcovBy_swap — Mathlib

English

Swapping the coordinates preserves weak cover: WCovBy(x.swap, y.swap) holds iff WCovBy(x, y).

Русский

Обмен координат сохраняет слабое покрытие: WCovBy(x.swap, y.swap) выполняется тогда и только тогда, когда WCovBy(x, y).

LaTeX

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

Lean4

@[simp]
theorem swap_wcovBy_swap : x.swap ⩿ y.swap ↔ x ⩿ y :=
  apply_wcovBy_apply_iff (OrderIso.prodComm : α × β ≃o β × α)

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