Documentation Verification Report

Defs

📁 Source: Mathlib/Data/Finite/Defs.lean

Statistics

Metric	Count
Definitions	0
Theorems `instFinite`, `finite_iff`, `infinite_iff`, `set_finite_iff`, `exists_equiv_fin`, `false`, `nonempty_decidableEq`, `not_infinite`, `ofBijective`, `of_equiv`, `of_not_infinite`, `finite_iff`, `false`, `not_finite`, `instFinite`, `not_infinite`, `to_subtype`, `not_finite`, `to_subtype`, `finite_coe_iff`, `finite_or_infinite`, `infinite_coe_iff`, `infinite_or_finite`, `not_finite`, `not_infinite`, `toFinite`, `finite_iff_exists_equiv_fin`, `finite_or_infinite`, `instFinitePLift`, `instFiniteULift`, `instInfinitePLift`, `instInfiniteULift`, `not_finite`, `not_finite_iff_infinite`, `not_infinite_iff_finite`	35
Total	35

Bool

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFinite` 📖	mathematical	—	`Finite`	—	—

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_iff` 📖	mathematical	—	`Finite`	—	`Finite.of_equiv`
`infinite_iff` 📖	mathematical	—	`Infinite`	—	`not_finite_iff_infinite` `Iff.not` `finite_iff`
`set_finite_iff` 📖	mathematical	—	`Set.Finite`	—	`finite_iff`

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_equiv_fin` 📖	mathematical	—	`Equiv`	—	`finite_iff_exists_equiv_fin`
`false` 📖	—	—	—	—	`not_finite`
`nonempty_decidableEq` 📖	—	—	—	—	`exists_equiv_fin`
`not_infinite` 📖	mathematical	—	`Infinite`	—	`not_infinite_iff_finite`
`ofBijective` 📖	mathematical	`Function.Bijective`	`Finite`	—	`Function.Bijective.finite_iff`
`of_equiv` 📖	mathematical	—	`Finite`	—	—
`of_not_infinite` 📖	mathematical	`Infinite`	`Finite`	—	`not_infinite_iff_finite`

Function.Bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_iff` 📖	mathematical	`Function.Bijective`	`Finite`	—	`Equiv.finite_iff`

Infinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`false` 📖	—	—	—	—	`not_finite`
`not_finite` 📖	mathematical	—	`Finite`	—	—

Prop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFinite` 📖	mathematical	—	`Finite`	—	`Finite.of_equiv` `Bool.instFinite`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_coe_iff` 📖	mathematical	—	`Finite` `Elem` `Finite`	—	—
`finite_or_infinite` 📖	mathematical	—	`Finite` `Infinite`	—	`em`
`infinite_coe_iff` 📖	mathematical	—	`Infinite` `Elem` `Infinite`	—	`not_finite_iff_infinite` `Iff.not` `finite_coe_iff`
`infinite_or_finite` 📖	mathematical	—	`Infinite` `Finite`	—	`em'`
`not_finite` 📖	mathematical	—	`Finite` `Infinite`	—	—
`not_infinite` 📖	mathematical	—	`Infinite` `Finite`	—	—
`toFinite` 📖	mathematical	—	`Finite`	—	—

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_infinite` 📖	mathematical	—	`Set.Infinite`	—	`Set.not_infinite`
`to_subtype` 📖	mathematical	—	`Finite` `Set.Elem`	—	—

Set.Infinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_finite` 📖	mathematical	`Set.Infinite`	`Set.Finite`	—	—
`to_subtype` 📖	mathematical	`Set.Infinite`	`Infinite` `Set.Elem`	—	`Set.infinite_coe_iff`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_iff_exists_equiv_fin` 📖	mathematical	—	`Finite` `Equiv`	—	—
`finite_or_infinite` 📖	mathematical	—	`Finite` `Infinite`	—	`not_finite_iff_infinite`
`instFinitePLift` 📖	mathematical	—	`Finite`	—	`Finite.of_equiv`
`instFiniteULift` 📖	mathematical	—	`Finite`	—	`Finite.of_equiv`
`instInfinitePLift` 📖	mathematical	—	`Infinite`	—	`Equiv.infinite_iff`
`instInfiniteULift` 📖	mathematical	—	`Infinite`	—	`Equiv.infinite_iff`
`not_finite` 📖	—	—	—	—	`Infinite.not_finite`
`not_finite_iff_infinite` 📖	mathematical	—	`Finite` `Infinite`	—	`Infinite.not_finite`
`not_infinite_iff_finite` 📖	mathematical	—	`Infinite` `Finite`	—	`Iff.not_right` `not_finite_iff_infinite`

---

← Back to Index