splitLower_ne_splitUpper — Mathlib

English

For any x, splitLower i x ≠ splitUpper i x.

Русский

Для любого x, splitLower i x ≠ splitUpper i x.

LaTeX

$$$I.splitLower i x \\neq I.splitUpper i x$$$

Lean4

theorem splitLower_ne_splitUpper (I : Box ι) (i : ι) (x : ℝ) : I.splitLower i x ≠ I.splitUpper i x :=
  by
  rcases le_or_gt x (I.lower i) with h | _
  · rw [splitUpper_eq_self.2 h, splitLower_eq_bot.2 h]
    exact WithBot.bot_ne_coe
  · refine (disjoint_splitLower_splitUpper I i x).ne ?_
    rwa [Ne, splitLower_eq_bot, not_le]

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