ofDual_covBy_ofDual_iff — Mathlib

English

In the dual order, CovBy relation mirrors CovBy with endpoints swapped.

Русский

В двойственном порядке CovBy зеркалирует CovBy с поменянными концами.

LaTeX

$$$$\forall {a,b:\alpha^{\mathrm{op}}},\ (\mathrm{CovBy}(a^{*},b^{*})\iff b^{*}\mathrm{CovBy} a^{*}).$$$$

Lean4

@[simp]
theorem ofDual_covBy_ofDual_iff {a b : αᵒᵈ} : ofDual a ⋖ ofDual b ↔ b ⋖ a :=
  and_congr_right' <| forall_congr' fun _ => forall_swap

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