A_mem_nhdsGT — Mathlib

English

If x ∈ A(f,L,r,ε), then A(f,L,r,ε) belongs to the right-sided neighborhood filter at x.

Русский

Если x ∈ A(f,L,r,ε), то A(f,L,r,ε) принадлежит к правой окрестности x.

LaTeX

$$$A f L r \\varepsilon \\in \\mathcal{N}_{x}^{>}$$$

Lean4

theorem A_mem_nhdsGT {L : F} {r ε x : ℝ} (hx : x ∈ A f L r ε) : A f L r ε ∈ 𝓝[>] x :=
  by
  rcases hx with ⟨r', rr', hr'⟩
  obtain ⟨s, s_gt, s_lt⟩ : ∃ s : ℝ, r / 2 < s ∧ s < r' := exists_between rr'.1
  have : s ∈ Ioc (r / 2) r := ⟨s_gt, le_of_lt (s_lt.trans_le rr'.2)⟩
  filter_upwards [Ioo_mem_nhdsGT <| show x < x + r' - s by linarith] with x' hx'
  use s, this
  have A : Icc x' (x' + s) ⊆ Icc x (x + r') :=
    by
    apply Icc_subset_Icc hx'.1.le
    linarith [hx'.2]
  intro y hy z hz
  exact hr' y (A hy) z (A hz)

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