inf_eq — Mathlib

English

In the dual order, CovBy corresponds to CovBy with reversed arguments: toDual b ⋖ toDual a iff a ⋖ b.

Русский

В двойственном порядке CovBy соответствует CovBy с обращёнными аргументами: toDual(b) ⋖ toDual(a) тогда и только тогда, когда a ⋖ b.

LaTeX

$$$$toDual\,b\,⋖\,toDual\,a\iff a\,⋖\,b.$$$$

Lean4

theorem inf_eq (hca : c ⩿ a) (hcb : c ⩿ b) (hab : a ≠ b) : a ⊓ b = c :=
  (le_inf hca.le hcb.le).eq_of_not_lt' fun h => hab.inf_lt_or_inf_lt.elim (hca.2 h) (hcb.2 h)

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