mem_uIcc — Mathlib

English

Membership of the unordered interval is characterized by a disjunction of two inequalities: a ∈ [[b,c]] iff (b ≤ a ∧ a ≤ c) ∨ (c ≤ a ∧ a ≤ b).

Русский

Принадлежность a к неупорядоченному интервалу [[b,c]] эквивалентна (b ≤ a ∧ a ≤ c) ∨ (c ≤ a ∧ 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]

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