inv_atBot₀ — Mathlib

English

The reciprocal of the neighborhood basis at 0 from the left equals atBot; i.e., inv nhdsLT 0 = atBot.

Русский

Обратное основание окрестности нуля слева равно atBot.

LaTeX

$$$(\mathcal{N}_{<0}(0))^{-1} = \mathrm{atBot}$$$

Lean4

@[simp]
theorem inv_atBot₀ : (atBot : Filter 𝕜)⁻¹ = 𝓝[<] 0 :=
  (((atBot_basis_Iio' (0 : 𝕜)).map _).comp_surjective inv_surjective).eq_of_same_basis <|
    (nhdsLT_basis _).congr (by simp) fun a ha ↦ by simp [inv_Iio₀ (inv_neg''.2 ha)]

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