Documentation

Mathlib.Topology.LocallyConstant.Algebra

Algebraic structure on locally constant functions #

This file puts algebraic structure (Group, AddGroup, etc) on the type of locally constant functions.

@[simp]
theorem LocallyConstant.coe_zero {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Zero Y] :
0 = 0
@[simp]
theorem LocallyConstant.coe_one {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [One Y] :
1 = 1
theorem LocallyConstant.zero_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Zero Y] (x : X) :
0 x = 0
theorem LocallyConstant.one_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [One Y] (x : X) :
1 x = 1
@[simp]
theorem LocallyConstant.coe_neg {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Neg Y] (f : LocallyConstant X Y) :
↑(-f) = -f
@[simp]
theorem LocallyConstant.coe_inv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Inv Y] (f : LocallyConstant X Y) :
f⁻¹ = (f)⁻¹
theorem LocallyConstant.neg_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Neg Y] (f : LocallyConstant X Y) (x : X) :
↑(-f) x = -f x
theorem LocallyConstant.inv_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Inv Y] (f : LocallyConstant X Y) (x : X) :
f⁻¹ x = (f x)⁻¹
@[simp]
theorem LocallyConstant.coe_add {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Add Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) :
↑(f + g) = f + g
@[simp]
theorem LocallyConstant.coe_mul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Mul Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) :
↑(f * g) = f * g
theorem LocallyConstant.add_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Add Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) (x : X) :
↑(f + g) x = f x + g x
theorem LocallyConstant.mul_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Mul Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) (x : X) :
↑(f * g) x = f x * g x
theorem LocallyConstant.instAddZeroClassLocallyConstant.proof_3 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddZeroClass Y] :
∀ (x x_1 : LocallyConstant X Y), ↑(x + x_1) = ↑(x + x_1)
theorem LocallyConstant.coeFnAddMonoidHom.proof_2 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddZeroClass Y] :
∀ (x x_1 : LocallyConstant X Y), ZeroHom.toFun { toFun := FunLike.coe, map_zero' := (_ : 0 = 0) } (x + x_1) = ZeroHom.toFun { toFun := FunLike.coe, map_zero' := (_ : 0 = 0) } (x + x_1)
@[simp]
theorem LocallyConstant.coeFnMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MulOneClass Y] :
∀ (a : LocallyConstant X Y) (a_1 : X), LocallyConstant.coeFnMonoidHom a a_1 = a a_1
@[simp]
theorem LocallyConstant.coeFnAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] :
∀ (a : LocallyConstant X Y) (a_1 : X), LocallyConstant.coeFnAddMonoidHom a a_1 = a a_1
theorem LocallyConstant.constAddMonoidHom.proof_2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] :
∀ (x x_1 : Y), ZeroHom.toFun { toFun := LocallyConstant.const X, map_zero' := (_ : LocallyConstant.const X 0 = LocallyConstant.const X 0) } (x + x_1) = ZeroHom.toFun { toFun := LocallyConstant.const X, map_zero' := (_ : LocallyConstant.const X 0 = LocallyConstant.const X 0) } (x + x_1)

The constant-function embedding, as an additive monoid hom.

Instances For
    @[simp]
    theorem LocallyConstant.constMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MulOneClass Y] (y : Y) :
    LocallyConstant.constMonoidHom y = LocallyConstant.const X y
    @[simp]
    theorem LocallyConstant.constAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] (y : Y) :
    LocallyConstant.constAddMonoidHom y = LocallyConstant.const X y

    The constant-function embedding, as a multiplicative monoid hom.

    Instances For
      noncomputable def LocallyConstant.charFn {X : Type u_1} (Y : Type u_2) [TopologicalSpace X] [MulZeroOneClass Y] {U : Set X} (hU : IsClopen U) :

      Characteristic functions are locally constant functions taking x : X to 1 if x ∈ U, where U is a clopen set, and 0 otherwise.

      Instances For
        theorem LocallyConstant.charFn_eq_one {X : Type u_1} (Y : Type u_2) [TopologicalSpace X] [MulZeroOneClass Y] {U : Set X} [Nontrivial Y] (x : X) (hU : IsClopen U) :
        ↑(LocallyConstant.charFn Y hU) x = 1 x U
        theorem LocallyConstant.charFn_eq_zero {X : Type u_1} (Y : Type u_2) [TopologicalSpace X] [MulZeroOneClass Y] {U : Set X} [Nontrivial Y] (x : X) (hU : IsClopen U) :
        ↑(LocallyConstant.charFn Y hU) x = 0 ¬x U
        theorem LocallyConstant.charFn_inj {X : Type u_1} (Y : Type u_2) [TopologicalSpace X] [MulZeroOneClass Y] {U : Set X} {V : Set X} [Nontrivial Y] (hU : IsClopen U) (hV : IsClopen V) (h : LocallyConstant.charFn Y hU = LocallyConstant.charFn Y hV) :
        U = V
        theorem LocallyConstant.coe_sub {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Sub Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) :
        ↑(f - g) = f - g
        theorem LocallyConstant.coe_div {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Div Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) :
        ↑(f / g) = f / g
        theorem LocallyConstant.sub_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Sub Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) (x : X) :
        ↑(f - g) x = f x - g x
        theorem LocallyConstant.div_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Div Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) (x : X) :
        ↑(f / g) x = f x / g x
        theorem LocallyConstant.instAddSemigroupLocallyConstant.proof_2 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddSemigroup Y] :
        ∀ (x x_1 : LocallyConstant X Y), ↑(x + x_1) = ↑(x + x_1)
        theorem LocallyConstant.instAddCommSemigroupLocallyConstant.proof_2 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommSemigroup Y] :
        ∀ (x x_1 : LocallyConstant X Y), ↑(x + x_1) = ↑(x + x_1)
        instance LocallyConstant.vadd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {α : Type u_3} [VAdd α Y] :
        instance LocallyConstant.smul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {α : Type u_3} [SMul α Y] :
        @[simp]
        theorem LocallyConstant.coe_vadd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [VAdd R Y] (r : R) (f : LocallyConstant X Y) :
        ↑(r +ᵥ f) = r +ᵥ f
        @[simp]
        theorem LocallyConstant.coe_smul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [SMul R Y] (r : R) (f : LocallyConstant X Y) :
        ↑(r f) = r f
        theorem LocallyConstant.vadd_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [VAdd R Y] (r : R) (f : LocallyConstant X Y) (x : X) :
        ↑(r +ᵥ f) x = r +ᵥ f x
        theorem LocallyConstant.smul_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [SMul R Y] (r : R) (f : LocallyConstant X Y) (x : X) :
        ↑(r f) x = r f x
        instance LocallyConstant.instPowLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {α : Type u_3} [Pow Y α] :
        theorem LocallyConstant.instAddMonoidLocallyConstant.proof_3 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddMonoid Y] :
        ∀ (x x_1 : LocallyConstant X Y), ↑(x + x_1) = ↑(x + x_1)
        theorem LocallyConstant.instAddMonoidLocallyConstant.proof_4 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddMonoid Y] :
        ∀ (x : LocallyConstant X Y) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
        theorem LocallyConstant.instAddCommMonoidLocallyConstant.proof_3 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommMonoid Y] :
        ∀ (x x_1 : LocallyConstant X Y), ↑(x + x_1) = ↑(x + x_1)
        theorem LocallyConstant.instAddCommMonoidLocallyConstant.proof_4 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommMonoid Y] :
        ∀ (x : LocallyConstant X Y) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
        theorem LocallyConstant.instAddGroupLocallyConstant.proof_6 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddGroup Y] :
        ∀ (x : LocallyConstant X Y) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
        theorem LocallyConstant.instAddGroupLocallyConstant.proof_5 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddGroup Y] :
        ∀ (x x_1 : LocallyConstant X Y), ↑(x - x_1) = ↑(x - x_1)
        theorem LocallyConstant.instAddGroupLocallyConstant.proof_7 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddGroup Y] :
        ∀ (x : LocallyConstant X Y) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
        theorem LocallyConstant.instAddGroupLocallyConstant.proof_3 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddGroup Y] :
        ∀ (x x_1 : LocallyConstant X Y), ↑(x + x_1) = ↑(x + x_1)
        theorem LocallyConstant.instAddGroupLocallyConstant.proof_4 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddGroup Y] :
        ∀ (x : LocallyConstant X Y), ↑(-x) = ↑(-x)
        theorem LocallyConstant.instAddCommGroupLocallyConstant.proof_7 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommGroup Y] :
        ∀ (x : LocallyConstant X Y) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
        theorem LocallyConstant.instAddCommGroupLocallyConstant.proof_6 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommGroup Y] :
        ∀ (x : LocallyConstant X Y) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
        theorem LocallyConstant.instAddCommGroupLocallyConstant.proof_5 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommGroup Y] :
        ∀ (x x_1 : LocallyConstant X Y), ↑(x - x_1) = ↑(x - x_1)
        theorem LocallyConstant.instAddCommGroupLocallyConstant.proof_3 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommGroup Y] :
        ∀ (x x_1 : LocallyConstant X Y), ↑(x + x_1) = ↑(x + x_1)
        @[simp]
        theorem LocallyConstant.constRingHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [NonAssocSemiring Y] (y : Y) :
        LocallyConstant.constRingHom y = LocallyConstant.const X y

        The constant-function embedding, as a ring hom.

        Instances For
          @[simp]
          theorem LocallyConstant.coe_algebraMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [CommSemiring R] [Semiring Y] [Algebra R Y] (r : R) :
          ↑(↑(algebraMap R (LocallyConstant X Y)) r) = ↑(algebraMap R (XY)) r
          @[simp]
          theorem LocallyConstant.coeFnRingHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Semiring Y] :
          ∀ (a : LocallyConstant X Y) (a_1 : X), LocallyConstant.coeFnRingHom a a_1 = a a_1

          FunLike.coe as a RingHom.

          Instances For
            @[simp]
            theorem LocallyConstant.coeFnₗ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [Semiring R] [AddCommMonoid Y] [Module R Y] :
            ∀ (a : LocallyConstant X Y) (a_1 : X), ↑(LocallyConstant.coeFnₗ R) a a_1 = a a_1
            def LocallyConstant.coeFnₗ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [Semiring R] [AddCommMonoid Y] [Module R Y] :

            FunLike.coe as a linear map.

            Instances For
              @[simp]
              theorem LocallyConstant.coeFnAlgHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [CommSemiring R] [Semiring Y] [Algebra R Y] :
              ∀ (a : LocallyConstant X Y) (a_1 : X), ↑(LocallyConstant.coeFnAlgHom R) a a_1 = a a_1
              def LocallyConstant.coeFnAlgHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [CommSemiring R] [Semiring Y] [Algebra R Y] :

              FunLike.coe as an AlgHom.

              Instances For

                Evaluation as an AddMonoidHom

                Instances For
                  @[simp]
                  theorem LocallyConstant.evalMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MulOneClass Y] (x : X) :
                  ∀ (a : LocallyConstant X Y), ↑(LocallyConstant.evalMonoidHom x) a = a x
                  @[simp]
                  theorem LocallyConstant.evalAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] (x : X) :
                  ∀ (a : LocallyConstant X Y), ↑(LocallyConstant.evalAddMonoidHom x) a = a x

                  Evaluation as a MonoidHom

                  Instances For
                    @[simp]
                    theorem LocallyConstant.evalₗ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [Semiring R] [AddCommMonoid Y] [Module R Y] (x : X) :
                    ∀ (a : LocallyConstant X Y), ↑(LocallyConstant.evalₗ R x) a = a x
                    def LocallyConstant.evalₗ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [Semiring R] [AddCommMonoid Y] [Module R Y] (x : X) :

                    Evaluation as a linear map

                    Instances For
                      @[simp]
                      theorem LocallyConstant.evalRingHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Semiring Y] (x : X) :
                      ∀ (a : LocallyConstant X Y), ↑(LocallyConstant.evalRingHom x) a = a x
                      def LocallyConstant.evalRingHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Semiring Y] (x : X) :

                      Evaluation as a RingHom

                      Instances For
                        @[simp]
                        theorem LocallyConstant.evalₐ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [CommSemiring R] [Semiring Y] [Algebra R Y] (x : X) :
                        ∀ (a : LocallyConstant X Y), ↑(LocallyConstant.evalₐ R x) a = a x
                        def LocallyConstant.evalₐ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [CommSemiring R] [Semiring Y] [Algebra R Y] (x : X) :

                        Evaluation as an AlgHom

                        Instances For
                          noncomputable def LocallyConstant.comapAddHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Add Z] (f : XY) (hf : Continuous f) :

                          LocallyConstant.comap as an AddHom.

                          Instances For
                            @[simp]
                            theorem LocallyConstant.comapAddHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Add Z] (f : XY) (hf : Continuous f) :
                            @[simp]
                            theorem LocallyConstant.comapMulHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Mul Z] (f : XY) (hf : Continuous f) :
                            noncomputable def LocallyConstant.comapMulHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Mul Z] (f : XY) (hf : Continuous f) :

                            LocallyConstant.comap as a MulHom.

                            Instances For
                              noncomputable def LocallyConstant.comapAddMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [AddZeroClass Z] (f : XY) (hf : Continuous f) :

                              LocallyConstant.comap as an AddMonoidHom.

                              Instances For
                                @[simp]
                                @[simp]
                                theorem LocallyConstant.comapMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [MulOneClass Z] (f : XY) (hf : Continuous f) :
                                noncomputable def LocallyConstant.comapMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [MulOneClass Z] (f : XY) (hf : Continuous f) :

                                LocallyConstant.comap as a MonoidHom.

                                Instances For
                                  @[simp]
                                  theorem LocallyConstant.comapₗ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [Semiring R] [AddCommMonoid Z] [Module R Z] (f : XY) (hf : Continuous f) :
                                  noncomputable def LocallyConstant.comapₗ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [Semiring R] [AddCommMonoid Z] [Module R Z] (f : XY) (hf : Continuous f) :

                                  LocallyConstant.comap as a linear map.

                                  Instances For
                                    @[simp]
                                    theorem LocallyConstant.comapRingHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Semiring Z] (f : XY) (hf : Continuous f) :
                                    noncomputable def LocallyConstant.comapRingHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Semiring Z] (f : XY) (hf : Continuous f) :

                                    LocallyConstant.comap as a RingHom.

                                    Instances For
                                      @[simp]
                                      theorem LocallyConstant.comapₐ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [CommSemiring R] [Semiring Z] [Algebra R Z] (f : XY) (hf : Continuous f) :
                                      noncomputable def LocallyConstant.comapₐ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [CommSemiring R] [Semiring Z] [Algebra R Z] (f : XY) (hf : Continuous f) :

                                      LocallyConstant.comap as an AlgHom

                                      Instances For
                                        theorem LocallyConstant.ker_comapₗ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [TopologicalSpace Y] {Z : Type u_4} [Semiring R] [AddCommMonoid Z] [Module R Z] (f : XY) (hf : Continuous f) (hfs : Function.Surjective f) :
                                        noncomputable def LocallyConstant.congrLeftAddEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Add Z] (e : X ≃ₜ Y) :

                                        LocallyConstant.congrLeft as an AddEquiv.

                                        Instances For
                                          noncomputable def LocallyConstant.congrLeftMulEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Mul Z] (e : X ≃ₜ Y) :

                                          LocallyConstant.congrLeft as a MulEquiv.

                                          Instances For
                                            @[simp]
                                            @[simp]
                                            theorem LocallyConstant.congrLeftₗ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [Semiring R] [AddCommMonoid Z] [Module R Z] (e : X ≃ₜ Y) :
                                            noncomputable def LocallyConstant.congrLeftₗ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [Semiring R] [AddCommMonoid Z] [Module R Z] (e : X ≃ₜ Y) :

                                            LocallyConstant.congrLeft as a linear equivalence.

                                            Instances For
                                              @[simp]
                                              theorem LocallyConstant.congrLeftₐ_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [CommSemiring R] [Semiring Z] [Algebra R Z] (e : X ≃ₜ Y) :
                                              @[simp]
                                              theorem LocallyConstant.congrLeftₐ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [CommSemiring R] [Semiring Z] [Algebra R Z] (e : X ≃ₜ Y) :
                                              noncomputable def LocallyConstant.congrLeftₐ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [CommSemiring R] [Semiring Z] [Algebra R Z] (e : X ≃ₜ Y) :

                                              LocallyConstant.congrLeft as an AlgEquiv.

                                              Instances For