mul_subset — Mathlib

English

For an open AddSubgroup U and r ∈ R, there exists an open AddSubgroup V such that r · V ⊆ U.

Русский

Для открытой подгруппы U и элемента r существует открытая подгруппа V такая, что r · V ⊆ U.

LaTeX

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

Lean4

/-- An open subgroup of a nonarchimedean ring contains the square of another one. -/
theorem mul_subset (U : OpenAddSubgroup R) : ∃ V : OpenAddSubgroup R, (V : Set R) * V ⊆ U :=
  by
  let ⟨V, H⟩ :=
    prod_self_subset <|
      (U.isOpen.preimage continuous_mul).mem_nhds <| by
        simpa only [Set.mem_preimage, Prod.snd_zero, mul_zero] using U.zero_mem
  use V
  rintro v ⟨a, ha, b, hb, hv⟩
  have hy := H (Set.mk_mem_prod ha hb)
  simp only [Set.mem_preimage, SetLike.mem_coe, hv] at hy
  rw [SetLike.mem_coe]
  exact hy

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