coe_splitLower — Mathlib

English

The Set form of splitLower is I.toSet ∩ {y | y_i ≤ x}.

Русский

Множество-форма splitLower: I.toSet ∩ {y | y_i ≤ x}.

LaTeX

$$$(splitLower I i x) = I^{\\;}(toSet) \\cap \\{ y : y_i \\le x \\}$$$

Lean4

@[simp]
theorem coe_splitLower : (splitLower I i x : Set (ι → ℝ)) = ↑I ∩ {y | y i ≤ x} :=
  by
  rw [splitLower, coe_mk']
  ext y
  simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and, ← Pi.le_def, le_update_iff,
    le_min_iff, and_assoc, and_forall_ne (p := fun j => y j ≤ upper I j) i, mem_def]
  rw [and_comm (a := y i ≤ x)]

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