Theorems · Theorem · Lie groups

ModuleFilterBasis.mk.injEq

∀ {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

0 results in Mathlib

Foundations

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

Assumes

SemiringTopologicalSpaceAddCommGroupModule