isOpen_A — Mathlib

English

For any L, r, ε, the set A(f, L, r, ε) is open in E.

Русский

Для любых L, r, ε множество A(f, L, r, ε) открыто в E.

LaTeX

$$$$\text{IsOpen}(A(f,L,r,\varepsilon)).$$$$

Lean4

theorem isOpen_A (L : E →L[𝕜] F) (r ε : ℝ) : IsOpen (A f L r ε) :=
  by
  rw [Metric.isOpen_iff]
  rintro x ⟨r', r'_mem, hr'⟩
  obtain ⟨s, s_gt, s_lt⟩ : ∃ s : ℝ, r / 2 < s ∧ s < r' := exists_between r'_mem.1
  have : s ∈ Ioc (r / 2) r := ⟨s_gt, le_of_lt (s_lt.trans_le r'_mem.2)⟩
  refine ⟨r' - s, by linarith, fun x' hx' => ⟨s, this, ?_⟩⟩
  have B : ball x' s ⊆ ball x r' := ball_subset (le_of_lt hx')
  intro y hy z hz
  exact hr' y (B hy) z (B hz)

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