FLT/Patching/Utils/InverseLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Inverse-limit utilities

Density and non-emptiness lemmas for inverse limits used in the patching argument.

Imports (3)
Imported by 5 files
  1. lemma dense_inverseLimit_of_forall_image_dense line 31 source

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

    Statement uses: Preorder, Nonempty, IsDirected, GE.ge, LE.le, TopologicalSpace, Continuous, Set, Subtype, Eq, Dense, Set.image

    Proof uses: Eq.mpr, IsOpen, Set.Nonempty, Inter.inter, id, congrArg, propext, dense_iff_inter_open, And, Set.preimage, Membership.mem, Finset, Exists, Set.pi, Iff.mp, isOpen_pi_iff, OrderDual, Finset.exists_le, Set.iInter, Subtype.property and 15 more

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  2. lemma denseRange_inverseLimit line 46 source

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

    Statement uses: Preorder, Nonempty, IsDirected, GE.ge, LE.le, TopologicalSpace, Continuous, Subtype, Eq, DenseRange

    Proof uses: dense_inverseLimit_of_forall_image_dense, Set.range, Eq.mpr, Dense, Set.image, Function.comp, id, congrArg, Set, Eq.symm, Set.range_comp

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  3. theorem nonempty_inverseLimit_of_finite line 67 source

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

    Statement uses: Preorder, LE.le, Eq, le_rfl, id, Function.comp, LE.le.trans, Nat, Antitone, Exists, Finite, Nonempty, Subtype

    Proof uses: CategoryTheory.Functor, Opposite, OrderDual, CategoryTheory.Functor.mk, Opposite.unop, Quiver.Hom, TypeCat.ofHom, Quiver.Hom.le, Quiver.Hom.unop, CategoryTheory.ConcreteCategory.ext, TypeCat.Fun, CategoryTheory.CategoryStruct.id, TypeCat.Fun.ext, CategoryTheory.ConcreteCategory.hom, funext, TypeCat.Fun.toFun, of_eq_true, Eq.trans, True, congr and 28 more

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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