FLT/Deformations/Algebra/InverseLimit/Topology.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Topology on inverse limits

The inverse limit of a system of topological algebraic structures inherits a natural topological structure as a subspace of the product. We record basic continuity properties of the canonical maps.

Imports (3)
Imported by 1 file
  1. instance InverseLimit.(instance at line 37) line 37 source
  2. lemma InverseLimit.val_continuous line 41 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Preorder, LE.le, FunLike, TopologicalSpace, Continuous, InverseLimit, Eq

    Proof uses: continuous_induced_dom

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  3. lemma InverseLimit.toComponent_continuous line 47 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Preorder, LE.le, FunLike, TopologicalSpace, Continuous, InverseLimit, InverseLimit.toComponent

    Proof uses: Eq.mpr, Eq, id, congrArg, InverseLimit.toComponent_def, Function.comp, rfl, Continuous.comp, continuous_apply, InverseLimit.val_continuous

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  4. lemma InverseLimit.lift_continuous line 58 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Preorder, LE.le, FunLike, TopologicalSpace, InverseLimit.InverseSystemHom, Continuous, InverseLimit, InverseLimit.lift

    Proof uses: Eq.mpr, Subtype.mk, Eq, id, congrArg, InverseLimit.lift_def, Continuous.subtype_mk, continuous_pi

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 25 steps

    Open to load the checked before-and-after goal states.

  5. instance InverseLimit.(instance at line 67) line 67 source
  6. instance InverseLimit.(instance at line 80) line 80 source
  7. instance InverseLimit.(instance at line 95) line 95 source