Untop0

📁 Source: Mathlib/Algebra/Order/WithTop/Untop0.lean

Statistics

Metric	Count
Definitions untop₀	1
Theorems coe_untop₀_of_ne_top, le_of_untop₀_le_untop₀, untopD_add, untop₀_add, untop₀_coe, untop₀_eq_zero, untop₀_le_untop₀, untop₀_le_untop₀_iff, untop₀_max, untop₀_min, untop₀_mul, untop₀_natCast, untop₀_neg, untop₀_nonneg, untop₀_ofNat, untop₀_top, untop₀_zero	17
Total	18

WithTop

Definitions

Name	Category	Theorems
untop₀ 📖	CompOp	19 math math: untop₀_ofNat, untop₀_natCast, untop₀_mul, untop₀_zero, untop₀_le_untop₀, untop₀_min, meromorphicOrderAt_ne_top_iff, untop₀_nonneg, untop₀_top, MeromorphicAt.tendsto_nhds_meromorphicTrailingCoeffAt, untop₀_add, untop₀_max, MeromorphicOn.divisor_apply, coe_untop₀_of_ne_top, untop₀_coe, untop₀_eq_zero, MeromorphicOn.divisor_def, untop₀_le_untop₀_iff, untop₀_neg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_untop₀_of_ne_top 📖	mathematical	—	some untop₀	—	ne_top_iff_exists
le_of_untop₀_le_untop₀ 📖	mathematical	Preorder.toLE PartialOrder.toPreorder untop₀ NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	WithTop instPreorder	—	CanLift.prf canLift
untopD_add 📖	mathematical	—	untopD WithTop add	—	CanLift.prf canLift
untop₀_add 📖	mathematical	—	untop₀ AddZero.toZero AddZeroClass.toAddZero WithTop add AddZero.toAdd	—	untopD_add
untop₀_coe 📖	mathematical	—	untop₀ some	—	—
untop₀_eq_zero 📖	mathematical	—	untop₀ WithTop zero Top.top top	—	—
untop₀_le_untop₀ 📖	mathematical	WithTop Preorder.toLE instPreorder PartialOrder.toPreorder	untop₀ NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	CanLift.prf canLift
untop₀_le_untop₀_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder untop₀ NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid WithTop instPreorder	—	CanLift.prf canLift
untop₀_max 📖	mathematical	—	untop₀ NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid WithTop SemilatticeSup.toMax semilatticeSup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	CanLift.prf canLift max_eq_right coe_le_coe max_eq_left LT.lt.le coe_lt_coe not_le
untop₀_min 📖	mathematical	—	untop₀ NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid WithTop SemilatticeInf.toMin semilatticeInf Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	CanLift.prf canLift
untop₀_mul 📖	mathematical	—	untop₀ MulZeroClass.toZero WithTop MulZeroClass.toMul instMulZeroClass	—	untopD_zero_mul
untop₀_natCast 📖	mathematical	—	untop₀ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid WithTop AddMonoidWithOne.toNatCast addMonoidWithOne	—	—
untop₀_neg 📖	mathematical	—	untop₀ NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid WithTop LinearOrderedAddCommGroup.instNeg NegZeroClass.toNeg	—	untop₀_top neg_zero
untop₀_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid untop₀ WithTop instPreorder zero	—	le_refl
untop₀_ofNat 📖	mathematical	—	untop₀ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid	—	—
untop₀_top 📖	mathematical	—	untop₀ Top.top WithTop top	—	—
untop₀_zero 📖	mathematical	—	untop₀ WithTop zero	—	—

---

← Back to Index