Documentation Verification Report

Defs

📁 Source: Mathlib/Logic/IsEmpty/Defs.lean

Statistics

Metric	Count
Definitions `elim`, `elim'`, `isEmptyElim`	3
Theorems `instIsEmpty`, `isEmpty`, `isEmpty'`, `isEmpty`, `isEmpty`, `exists_iff`, `false`, `forall_iff`, `instSubsingleton`, `prop_iff`, `instIsEmpty`, `isEmpty_left`, `isEmpty_right`, `isEmpty_left`, `isEmpty_right`, `instIsEmpty`, `instIsEmpty`, `isEmpty_left`, `isEmpty_false`, `isEmpty_of_false`, `instIsEmptyFalse`, `instIsEmptyForallOfNonempty`, `instIsEmptyPSum`, `instIsEmptySubtype`, `instIsEmptySum`, `isEmpty_iff`	26
Total	29

Empty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsEmpty` 📖	mathematical	—	`IsEmpty`	—	—

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEmpty` 📖	mathematical	—	`IsEmpty`	—	—
`isEmpty'` 📖	mathematical	—	`IsEmpty`	—	`isEmpty`

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEmpty` 📖	mathematical	—	`IsEmpty`	—	`IsEmpty.false`

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEmpty` 📖	mathematical	—	`IsEmpty`	—	`IsEmpty.false`

IsEmpty

Definitions

Name	Category	Theorems
`elim` 📖	CompOp	2 math math: `Quotient.finLiftOn_empty`, `Trunc.finLiftOn_empty`
`elim'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_iff` 📖	—	—	—	—	`false`
`false` 📖	—	—	—	—	—
`forall_iff` 📖	—	—	—	—	—
`instSubsingleton` 📖	—	—	—	—	—
`prop_iff` 📖	mathematical	—	`IsEmpty`	—	`isEmpty_iff`

PEmpty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsEmpty` 📖	mathematical	—	`IsEmpty`	—	—

PProd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEmpty_left` 📖	mathematical	—	`IsEmpty`	—	`Function.isEmpty`
`isEmpty_right` 📖	mathematical	—	`IsEmpty`	—	`Function.isEmpty`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEmpty_left` 📖	mathematical	—	`IsEmpty`	—	`Function.isEmpty`
`isEmpty_right` 📖	mathematical	—	`IsEmpty`	—	`Function.isEmpty`

Quot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsEmpty` 📖	mathematical	—	`IsEmpty`	—	`Function.Surjective.isEmpty`

Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsEmpty` 📖	mathematical	—	`IsEmpty`	—	`Quot.instIsEmpty`

Sigma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEmpty_left` 📖	mathematical	—	`IsEmpty`	—	`Function.isEmpty`

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEmpty_false` 📖	mathematical	—	`IsEmpty`	—	`isEmpty_of_false`
`isEmpty_of_false` 📖	mathematical	—	`IsEmpty`	—	—

(root)

Definitions

Name	Category	Theorems
`isEmptyElim` 📖	CompOp	12 math math: `MvPolynomial.isEmptyRingEquiv_apply`, `MeasureTheory.Measure.pi_of_empty`, `FirstOrder.Language.LHom.ofIsEmpty_onRelation`, `MeasureTheory.Measure.volume_pi_eq_dirac`, `PiTensorProduct.isEmptyEquiv_symm_apply`, `MvPolynomial.isEmptyAlgEquiv_apply`, `FirstOrder.Language.orderLHom_onFunction`, `OrderEmbedding.coe_ofIsEmpty`, `FirstOrder.Language.LHom.ofIsEmpty_onFunction`, `Homeomorph.sumEmpty_apply`, `OrderEmbedding.ofIsEmpty_apply`, `RelIso.sumLexEmpty_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsEmptyFalse` 📖	mathematical	—	`IsEmpty`	—	—
`instIsEmptyForallOfNonempty` 📖	—	`IsEmpty`	—	—	`Function.isEmpty`
`instIsEmptyPSum` 📖	mathematical	—	`IsEmpty`	—	`IsEmpty.false`
`instIsEmptySubtype` 📖	mathematical	—	`IsEmpty`	—	`IsEmpty.false`
`instIsEmptySum` 📖	mathematical	—	`IsEmpty`	—	`IsEmpty.false`
`isEmpty_iff` 📖	mathematical	—	`IsEmpty`	—	`IsEmpty.false`

---

← Back to Index