coe_eq_of_mem_split_of_mem_le — Mathlib

English

If J belongs to split I i x and y ∈ J with y_i ≤ x, then J as a set equals I’s set intersected with {y | y_i ≤ x}.

Русский

Если J принадлежит split I i x и существует y ∈ J с y_i ≤ x, то множество J равно множеству I пересеченному с {y | y_i ≤ x}.

LaTeX

$$$(J : \\mathrm{Set}(\\iota \\to \\mathbb{R})) = \\uparrow I \\cap \\{y \\mid y_i \\le x\\}$$$

Lean4

theorem coe_eq_of_mem_split_of_mem_le {y : ι → ℝ} (h₁ : J ∈ split I i x) (h₂ : y ∈ J) (h₃ : y i ≤ x) :
    (J : Set (ι → ℝ)) = ↑I ∩ {y | y i ≤ x} :=
  by
  refine (mem_split_iff'.1 h₁).resolve_right fun H => ?_
  rw [← Box.mem_coe, H] at h₂
  exact h₃.not_gt h₂.2

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