mem_split_iff' — Mathlib

English

A box J lies in the split I i x exactly when its underlying set equals I’s set intersected with {y | y_i ≤ x} or with {y | x < y_i}.

Русский

Коробка J лежит в split I i x точно тогда, когда множество J как подмножество равно множеству I ∩ {y | y_i ≤ x} или I ∩ {y | x < y_i}.

LaTeX

$$$J^{\\mathrm{toSet}} = I^{\\mathrm{toSet}} \\cap \\{y : y_i \\le x\\} \\quad\\text{или}\\quad J^{\\mathrm{toSet}} = I^{\\mathrm{toSet}} \\cap \\{y : x < y_i\\}$$$

Lean4

theorem mem_split_iff' :
    J ∈ split I i x ↔ (J : Set (ι → ℝ)) = ↑I ∩ {y | y i ≤ x} ∨ (J : Set (ι → ℝ)) = ↑I ∩ {y | x < y i} := by
  simp [mem_split_iff, ← Box.withBotCoe_inj]

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