mem_uIoc — Mathlib

English

A belongs to the unordered interval between b and c if and only if either b < a ≤ c with a between, or c < a ≤ b with a between.

Русский

Элемент a принадлежит неупорядоченному интервалу между b и c тогда и только тогда, когда либо b < a ≤ c, либо c < a ≤ b.

LaTeX

$$$ a \\in Ι(b,c) \\iff (b < a \\land a \\le c) \\lor (c < a \\land a \\le b) $$$

Lean4

theorem mem_uIoc : a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b := by rw [uIoc_eq_union, mem_union, mem_Ioc, mem_Ioc]

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