left_mul_subset — Mathlib

English

An open additive subgroup U in a nonarchimedean ring contains the product V · V for some open additive subgroup V.

Русский

Открытая аддитивная подгруппа U в неархимедовом кольце содержит произведение V · V для некоторой открытой подгруппы V.

LaTeX

$$∃ V : OpenAddSubgroup R, (V : Set R) * V ⊆ U$$

Lean4

/-- Given an open subgroup `U` and an element `r` of a nonarchimedean ring, there is an open
  subgroup `V` such that `r • V` is contained in `U`. -/
theorem left_mul_subset (U : OpenAddSubgroup R) (r : R) : ∃ V : OpenAddSubgroup R, r • (V : Set R) ⊆ U :=
  ⟨U.comap (AddMonoidHom.mulLeft r) (continuous_mul_left r), (U : Set R).image_preimage_subset _⟩

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