eq_of_notMem_uIoc_of_notMem_uIoc — Mathlib

English

If a ≤ c and b ≤ c and a ∉ Ι(b,c) and b ∉ Ι(a,c), then a = b.

Русский

Если a ≤ c и b ≤ c и a ∉ Ι(b,c) и b ∉ Ι(a,c), тогда a = b.

LaTeX

$$$ (a \\le c) \\land (b \\le c) \\land a \\notin Ι(b,c) \\land b \\notin Ι(a,c) \\implies a = b $$$

Lean4

theorem eq_of_notMem_uIoc_of_notMem_uIoc (ha : a ≤ c) (hb : b ≤ c) : a ∉ Ι b c → b ∉ Ι a c → a = b :=
  by
  simp_rw [notMem_uIoc]
  rintro (⟨_, _⟩ | ⟨_, _⟩) (⟨_, _⟩ | ⟨_, _⟩) <;> apply le_antisymm <;>
    first
    | assumption
    | exact le_of_lt ‹_›
    | exact absurd hb (not_le_of_gt ‹c < b›)
    | exact absurd ha (not_le_of_gt ‹c < a›)

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