English
For a given x, the map J ↦ { i ∈ ι | J.lower(i) = x(i) } is injective on the set { J | J ∈ π ∧ x ∈ Box.Icc(J) }.
Русский
Для данного x отображение J ↦ { i ∈ ι | J.lower(i) = x(i) } является инъективным на множестве { J | J ∈ π и x ∈ Box.Icc(J) }.
LaTeX
$$$\text{InjOn} \big( J \mapsto \{ i \mid J.lower(i) = x(i) \} \big) \big( \{ J \mid J \in \pi \land x \in Box.Icc(J) \} \big)$$$
Lean4
/-- An auxiliary lemma used to prove that the same point can't belong to more than
`2 ^ Fintype.card ι` closed boxes of a prepartition. -/
theorem injOn_setOf_mem_Icc_setOf_lower_eq (x : ι → ℝ) :
InjOn (fun J : Box ι => {i | J.lower i = x i}) {J | J ∈ π ∧ x ∈ Box.Icc J} :=
by
rintro J₁ ⟨h₁, hx₁⟩ J₂ ⟨h₂, hx₂⟩ (H : {i | J₁.lower i = x i} = {i | J₂.lower i = x i})
suffices ∀ i, (Ioc (J₁.lower i) (J₁.upper i) ∩ Ioc (J₂.lower i) (J₂.upper i)).Nonempty
by
choose y hy₁ hy₂ using this
exact π.eq_of_mem_of_mem h₁ h₂ hy₁ hy₂
intro i
simp only [Set.ext_iff, mem_setOf] at H
rcases (hx₁.1 i).eq_or_lt with hi₁ | hi₁
· have hi₂ : J₂.lower i = x i := (H _).1 hi₁
have H₁ : x i < J₁.upper i := by simpa only [hi₁] using J₁.lower_lt_upper i
have H₂ : x i < J₂.upper i := by simpa only [hi₂] using J₂.lower_lt_upper i
rw [Set.Ioc_inter_Ioc, hi₁, hi₂, sup_idem, Set.nonempty_Ioc]
exact lt_min H₁ H₂
· have hi₂ : J₂.lower i < x i := (hx₂.1 i).lt_of_ne (mt (H _).2 hi₁.ne)
exact ⟨x i, ⟨hi₁, hx₁.2 i⟩, ⟨hi₂, hx₂.2 i⟩⟩
