Theorems · Inductive type · geometry

ContinuousAffineEquiv

(k : Type u_1) →
  (P₁ : Type u_2) →
    (P₂ : Type u_3) →
      {V₁ : Type u_4} →
        {V₂ : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [Module k V₁] →
                [AddTorsor V₁ P₁] →
                  [TopologicalSpace P₁] →
                    [inst_5 : AddCommGroup V₂] →
                      [Module k V₂] → [AddTorsor V₂ P₂] → [TopologicalSpace P₂] → Type (max (max (max u_2 u_3) u_4) u_5)

A continuous affine equivalence, denoted P₁ ≃ᴬ[k] P₂, between two affine topological spaces is an affine equivalence such that forward and inverse maps are continuous.

Defined in

Mathlib.Topology.Algebra.ContinuousAffineEquiv

Cited by

90 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

RingAddCommGroupModuleAddTorsorTopologicalSpaceAddCommGroupModuleAddTorsorTopologicalSpace