bihimp_of_le — Mathlib

English

If a ≤ b, then bihimp(a, b) = himp(b, a); i.e., the bihimp reduces to the implication when the first argument is below the second.

Русский

Если a ≤ b, то bihimp(a,b) = imply(b,a); то есть биимп переходит к импликации при a ≤ b.

LaTeX

$$$a \le b \Rightarrow \operatorname{bihimp}(a,b) = \operatorname{himp}(b,a)$$$

Lean4

theorem bihimp_of_le {a b : α} (h : a ≤ b) : a ⇔ b = b ⇨ a := by rw [bihimp, himp_eq_top_iff.2 h, inf_top_eq]

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