Theorems · Definition · Lie groups

ModuleFilterBasis.mk.noConfusion

{R : Type u_1} →
  {M : Type u_2} →
    {inst : Semiring R} →
      {inst_1 : TopologicalSpace R} →
        {inst_2 : AddCommGroup M} →
          {inst_3 : Module R M} →
            {P : Sort u} →
              {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' : 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 := toAddGroupFilterBasis, smul' := smul',
                                    smul_left' := smul_left', smul_right' := smul_right' } =
                                  { toAddGroupFilterBasis := toAddGroupFilterBasis', smul' := smul'',
                                    smul_left' := smul_left'', smul_right' := smul_right'' } →
                                (toAddGroupFilterBasis ≍ toAddGroupFilterBasis' → P) → P

Defined in

Mathlib.Topology.Algebra.FilterBasis

Cited by

1 results in Mathlib

Foundations

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