exists_mem_splitCenterBox — Mathlib

English

For every x, there exists s such that x ∈ I.splitCenterBox s iff x ∈ I.

Русский

Для каждого x существует такое s, что x ∈ I.splitCenterBox s тогда и только тогда, когда x ∈ I.

LaTeX

$$$$\exists s, x \in I.splitCenterBox s \;\iff\; x \in I.$$$$

Lean4

@[simp]
theorem exists_mem_splitCenterBox {I : Box ι} {x : ι → ℝ} : (∃ s, x ∈ I.splitCenterBox s) ↔ x ∈ I :=
  ⟨fun ⟨s, hs⟩ ↦ I.splitCenterBox_le s hs, fun hx ↦
    ⟨{i | (I.lower i + I.upper i) / 2 < x i}, mem_splitCenterBox.2 ⟨hx, fun _ ↦ Iff.rfl⟩⟩⟩

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