Lift

📁 Source: Mathlib/Tactic/Lift.lean

Statistics

Metric	Count
Definitions CanLift, getInst, main, Lift	4
Theorems prf, canLift, canLift, canLift', instCanLift, canLift, exists_pi_extension, instCanLiftIntNatCastLeOfNat	8
Total	12

CanLift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prf 📖	—	—	—	—	—

Mathlib.Tactic.Lift

Definitions

Name	Category	Theorems
getInst 📖	CompOp	—
main 📖	CompOp	—

PSet

Definitions

Name	Category	Theorems
Lift 📖	CompOp	1 math math: lift_mem_embed

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canLift 📖	—	CanLift	—	—	CanLift.prf

PiSubtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canLift 📖	mathematical	—	CanLift	—	Subtype.exists_pi_extension
canLift' 📖	mathematical	—	CanLift	—	canLift

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCanLift 📖	mathematical	—	CanLift	—	CanLift.prf

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canLift 📖	mathematical	—	CanLift	—	—
exists_pi_extension 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
CanLift 📖	CompData	84 math math: LieSubmodule.instCanLiftSubmoduleToSubmoduleForallForallForallMemBracket, NonUnitalSubalgebra.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMul, TopologicalSpace.OpenNhdsOf.canLiftSet, ENNReal.canLift, QuadraticMap.canLift, ConvexCone.canLift, Subring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallNeg, PiSubtype.canLift', Ideal.instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided, ContinuousMapZero.instCanLift, NNReal.canLift, NonUnitalStarSubalgebra.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMulForallForallStar, Submonoid.instCanLiftSetCoeAndMemOfNatForallForallForallForallHMul, Int.canLiftPNat, UpperHalfPlane.canLift, ENat.canLift, Multiset.canLiftFinset, NNRat.canLift, Finset.FinsetCoe.canLift, TopologicalSpace.Compacts.instCanLiftSetCoeIsCompact, StarSubsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallStar, EReal.canLift, Nat.canLiftPNat, Cardinal.instCanLiftENatOfENatLeAleph0, TopologicalSpace.IrreducibleCloseds.instCanLiftSetCoeAndIsIrreducibleIsClosed, instCanLiftAddUnitsValIsAddUnit, EReal.instCanLiftENNRealToERealLeOfNat, OnePoint.canLift, Unitization.instCanLift, Subgroup.instCanLiftSetCoeAndMemOfNatForallForallForallForallHMulForallForallInv, AddSubsemigroup.instCanLiftSetCoeForallForallForallMemForallHAdd, Subsemigroup.instCanLiftSetCoeForallForallForallMemForallHMul, Filter.canLift, Complex.UnitDisc.instCanLiftCoeLtRealNormOfNat, NonUnitalSubring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallNeg, Interval.canLift, NNReal.ContinuousMap.canLift, NonUnitalStarSubsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallStar, PartENat.instCanLiftNatCastDom, Multiset.canLift, AddSubgroup.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallNeg, OrderHom.canLift, WithOne.instCanLift, Finset.canLift, NonemptyInterval.instCanLift, WithZero.instCanLiftMultiplicativeExpNeOfNat, QuadraticMap.canLift', Set.PiSetCoe.canLift, ContinuousMap.canLift, NonUnitalSubsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMul, Subtype.canLift, PointedCone.canLift, WithTop.canLift, LinearEquiv.canLiftContinuousLinearEquiv, Finset.PiFinsetCoe.canLift, WithBot.canLift, ClosedSubmodule.instCanLiftSubmoduleToSubmoduleIsClosedCoe, Prod.instCanLift, Set.instCanLiftFinsetCoeFinite, Rat.canLift, Set.PiSetCoe.canLift', Cardinal.canLiftCardinalNat, Submodule.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallHSMul, Complex.canLift, StarSubalgebra.instCanLiftSetCoeAndForallForallForallMemForallHAddForallForallForallForallHMulForallCoeRingHomAlgebraMapForallForallStar, Equiv.instCanLiftForallCoeBijective, Fin.instCanLiftNatValLt, Cardinal.canLiftCardinalType, Finset.PiFinsetCoe.canLift', instCanLiftUnitsValIsUnit, Subalgebra.instCanLiftSetCoeAndForallForallForallMemForallHAddForallForallForallForallHMulForallCoeRingHomAlgebraMap, Set.canLift, AddSubmonoid.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAdd, Subsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMul, instCanLiftIntNatCastLeOfNat, LinearMap.canLiftContinuousLinearMap, TopologicalSpace.Closeds.instCanLiftSetCoeIsClosed, Function.instCanLiftForallEmbeddingCoeInjective, Finsupp.instCanLift, PiSubtype.canLift, TopologicalSpace.Opens.instCanLiftSetCoeIsOpen, WithZero.instCanLift, List.canLift, ContinuousMap.instCanLiftForallCoeContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCanLiftIntNatCastLeOfNat 📖	mathematical	—	CanLift	—	—

---

← Back to Index