Theorems · Theorem · Lie groups

ModuleFilterBasis.mk.inj

∀ {R : Type u_1} {M : Type u_2} {inst : Semiring R} {inst_1 : TopologicalSpace R} {inst_2 : AddCommGroup M}
  {inst_3 : Module R M} {toAddGroupFilterBasis : AddGroupFilterBasis M}
  {smul' : ∀ {U : Set M}, U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ nhds 0, ∃ W ∈ toAddGroupFilterBasis.sets, V • W ⊆ U}
  {smul_left' :
    ∀ (x₀ : R) {U : Set M},
      U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ toAddGroupFilterBasis.sets, V ⊆ (fun x => x₀ • x) ⁻¹' U}
  {smul_right' : ∀ (m₀ : M) {U : Set M}, U ∈ toAddGroupFilterBasis.sets → ∀ᶠ (x : R) in nhds 0, x • m₀ ∈ U}
  {toAddGroupFilterBasis_1 : AddGroupFilterBasis M}
  {smul'_1 :
    ∀ {U : Set M}, U ∈ toAddGroupFilterBasis_1.sets → ∃ V ∈ nhds 0, ∃ W ∈ toAddGroupFilterBasis_1.sets, V • W ⊆ U}
  {smul_left'_1 :
    ∀ (x₀ : R) {U : Set M},
      U ∈ toAddGroupFilterBasis_1.sets → ∃ V ∈ toAddGroupFilterBasis_1.sets, V ⊆ (fun x => x₀ • x) ⁻¹' U}
  {smul_right'_1 : ∀ (m₀ : M) {U : Set M}, U ∈ toAddGroupFilterBasis_1.sets → ∀ᶠ (x : R) in nhds 0, x • m₀ ∈ U},
  { toAddGroupFilterBasis := toAddGroupFilterBasis, smul' := smul', smul_left' := smul_left',
        smul_right' := smul_right' } =
      { toAddGroupFilterBasis := toAddGroupFilterBasis_1, smul' := smul'_1, smul_left' := smul_left'_1,
        smul_right' := smul_right'_1 } →
    toAddGroupFilterBasis = toAddGroupFilterBasis_1

Defined in

Mathlib.Topology.Algebra.FilterBasis

Cited by

1 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Quot.sound