coe_eq_of_mem_split_of_lt_mem — Mathlib

English

Analogous to the lower piece, if J ∈ split I i x and y ∈ J with x < y_i, then J equals I ∩ {y | x < y_i}.

Русский

Аналогично нижнему куску: если J ∈ split I i x и y ∈ J с x < y_i, то J = I ∩ {y | x < y_i}.

LaTeX

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

Lean4

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

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