bihimp_of_ge — Mathlib

English

If b ≤ a, then bihimp(a, b) = himp(a, b); the bihimp coincides with the implication when the second argument is below the first.

Русский

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

LaTeX

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

Lean4

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

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