notMem_uIoc — Mathlib

English

Characterization of non-membership: a ∉ Ι(b,c) if and only if either a ≤ b and a ≤ c, or c < a and b < a.

Русский

Характеризация не принадлежности: a ∉ Ι(b,c) тогда и только тогда, когда a ≤ b и a ≤ c, или c < a и b < a.

LaTeX

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

Lean4

theorem notMem_uIoc : a ∉ Ι b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a :=
  by
  simp only [uIoc_eq_union, mem_union, mem_Ioc, ← not_le]
  tauto

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