mem_uIcc' — Mathlib

English

Membership in uIcc is characterized by a pair of lattice inequalities; specifically, a ∈ [[b,c]] iff (b ≤ a ≤ c) or (c ≤ a ≤ b).

Русский

Членство в uIcc охарактеризуется парой неравенств: a ∈ [[b,c]] тогда и только тогда, когда (b ≤ a ≤ c) или (c ≤ a ≤ b).

LaTeX

$$$a \in [[b, c]] \iff (b \le a \land a \le c) \lor (c \le a \land a \le b)$$$

Lean4

theorem mem_uIcc' : a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b := by simp [uIcc_eq_union]

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