le_bihimp — Mathlib

English

If a ⊓ b ≤ c and a ⊓ c ≤ b, then a ≤ b if and only if c. In other words, under these two compatibility conditions between a, b, and c, the order between a and b is determined by c.

Русский

Пусть a ⊓ b ≤ c и a ⊓ c ≤ b; тогда a ≤ b, если и только если c. Иными словами, при выполнении двух условий совместимости порядок между a и b определяется через c.

LaTeX

$$$(a \wedge b \le c) \land (a \wedge c \le b) \Rightarrow\ (a \le b \iff c)$$$

Lean4

theorem le_bihimp {a b c : α} (hb : a ⊓ b ≤ c) (hc : a ⊓ c ≤ b) : a ≤ b ⇔ c :=
  le_inf (le_himp_iff.2 hc) <| le_himp_iff.2 hb

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