toDual_wcovBy_toDual_iff — Mathlib

English

In the dual order, the cover relation reverses: b under dual covers a under dual iff a covers b in the original order.

Русский

В двойственном порядке отношение покрытия разворачивается: b покрывает a в двойственном порядке тогда и только тогда, когда a покрывает b в исходном порядке.

LaTeX

$$$$\forall {\alpha} [\text{Preorder }\alpha],\ a,b:\alpha,\; toDual(b)⩿toDual(a)\iff a⩿b.$$$$

Lean4

@[simp]
theorem toDual_wcovBy_toDual_iff : toDual b ⩿ toDual a ↔ a ⩿ b :=
  and_congr_right' <| forall_congr' fun _ => forall_swap

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