notMem_uIcc_of_gt — Mathlib

English

Let a,b,c be elements of a linearly ordered set. If a < c and b < c, then c is not contained in the unordered closed interval between a and b.

Русский

Пусть a, b, c принадлежат линейному порядку. Если a < c и b < c, то c не принадлежит неупорядоченному замкнутому интервалу между a и b.

LaTeX

$$$ (a < c) \\land (b < c) \\implies c \\notin [[a,b]] $$$

Lean4

theorem notMem_uIcc_of_gt (ha : a < c) (hb : b < c) : c ∉ [[a, b]] :=
  notMem_Icc_of_gt <| max_lt_iff.mpr ⟨ha, hb⟩

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