comap_mulLeft_nhdsGT_zero — Mathlib

English

Left-multiplication by a positive factor preserves the nhds from above of zero.

Русский

Левая домножение на положительный множитель сохраняет окрестности слева от нуля.

LaTeX

$$For x > 0, comap (fun t => x * t) (𝓝[>] 0) = 𝓝[>] 0.$$

Lean4

theorem comap_mulLeft_nhdsGT_zero {x : 𝕜} (hx : 0 < x) : comap (x * ·) (𝓝[>] 0) = 𝓝[>] 0 :=
  by
  rw [nhdsWithin, comap_inf, comap_principal, preimage_const_mul_Ioi _ hx, zero_div]
  congr 1
  refine ((Homeomorph.mulLeft₀ x hx.ne').comap_nhds_eq _).trans ?_
  simp

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