disjoint_splitLower_splitUpper — Mathlib

English

The two parts splitLower and splitUpper are disjoint.

Русский

Две части splitLower и splitUpper обладают взаимно‑декартами (не пересекаются).

LaTeX

$$$\\text{Disjoint}(I.splitLower i x, I.splitUpper i x)$$$

Lean4

theorem disjoint_splitLower_splitUpper (I : Box ι) (i : ι) (x : ℝ) : Disjoint (I.splitLower i x) (I.splitUpper i x) :=
  by
  rw [← disjoint_withBotCoe, coe_splitLower, coe_splitUpper]
  refine (Disjoint.inf_left' _ ?_).inf_right' _
  rw [Set.disjoint_left]
  exact fun y (hle : y i ≤ x) hlt => not_lt_of_ge hle hlt

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