B_mem_nhdsGT — Mathlib

English

If x ∈ B(f,K,r,s,ε), then B(f,K,r,s,ε) lies in the right-sided neighborhood at x.

Русский

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

LaTeX

$$$B f K r s ε \\in \\mathcal{N}_{x}^{>}$$$

Lean4

theorem B_mem_nhdsGT {K : Set F} {r s ε x : ℝ} (hx : x ∈ B f K r s ε) : B f K r s ε ∈ 𝓝[>] x :=
  by
  obtain ⟨L, LK, hL₁, hL₂⟩ : ∃ L : F, L ∈ K ∧ x ∈ A f L r ε ∧ x ∈ A f L s ε := by
    simpa only [B, mem_iUnion, mem_inter_iff, exists_prop] using hx
  filter_upwards [A_mem_nhdsGT hL₁, A_mem_nhdsGT hL₂] with y hy₁ hy₂
  simp only [B, mem_iUnion, mem_inter_iff, exists_prop]
  exact ⟨L, LK, hy₁, hy₂⟩

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