ofDual_wcovBy_ofDual_iff — Mathlib

English

In the dual order, a is covered by b iff b is covered by a in the original order.

Русский

Во двойственном порядке a покрывает b тогда, когда b покрывает a в исходном порядке.

LaTeX

$$$$\forall {a,b:\alpha^{\mathrm{op}}},\ onDual(a)\;\mathrel{⩿}\; onDual(b)\iff b\mathrel{⩿}a.$$$$

Lean4

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

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