Basic

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

Statistics

Metric	Count
Definitions	0
Theorems `of_isEmpty`, `of_isEmpty`, `extend_of_isEmpty`, `not_surjective_of_isEmpty_of_nonempty`, `surjective_iff_isEmpty`, `biTotal_empty`, `biTotal_iff_isEmpty_left`, `biTotal_iff_isEmpty_right`, `isEmpty_Prop`, `isEmpty_fun`, `isEmpty_or_nonempty`, `isEmpty_pi`, `isEmpty_plift`, `isEmpty_pprod`, `isEmpty_prod`, `isEmpty_psigma`, `isEmpty_psum`, `isEmpty_sigma`, `isEmpty_subtype`, `isEmpty_sum`, `isEmpty_ulift`, `leftTotal_empty`, `leftTotal_iff_isEmpty_left`, `nonempty_fun`, `not_isEmpty_iff`, `not_isEmpty_of_nonempty`, `not_nonempty_iff`, `rightTotal_empty`, `rightTotal_iff_isEmpty_right`, `wellFounded_of_isEmpty`	30
Total	30

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extend_of_isEmpty` 📖	mathematical	—	`extend`	—	`extend_apply'`
`not_surjective_of_isEmpty_of_nonempty` 📖	—	—	—	—	`not_isEmpty_of_nonempty` `Surjective.isEmpty`
`surjective_iff_isEmpty` 📖	mathematical	—	`IsEmpty`	—	`Surjective.isEmpty` `Surjective.of_isEmpty`

Function.Bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isEmpty` 📖	mathematical	—	`Function.Bijective`	—	`Function.isEmpty` `Function.injective_of_subsingleton` `IsEmpty.instSubsingleton` `Function.Surjective.of_isEmpty`

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isEmpty` 📖	—	—	—	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biTotal_empty` 📖	mathematical	—	`Relator.BiTotal`	—	`leftTotal_empty` `rightTotal_empty`
`biTotal_iff_isEmpty_left` 📖	mathematical	—	`Relator.BiTotal` `IsEmpty`	—	—
`biTotal_iff_isEmpty_right` 📖	mathematical	—	`Relator.BiTotal` `IsEmpty`	—	—
`isEmpty_Prop` 📖	mathematical	—	`IsEmpty`	—	—
`isEmpty_fun` 📖	mathematical	—	`IsEmpty`	—	`isEmpty_pi` `exists_true_iff_nonempty`
`isEmpty_or_nonempty` 📖	mathematical	—	`IsEmpty`	—	`em` `not_isEmpty_iff`
`isEmpty_pi` 📖	mathematical	—	`IsEmpty`	—	—
`isEmpty_plift` 📖	mathematical	—	`IsEmpty`	—	—
`isEmpty_pprod` 📖	mathematical	—	`IsEmpty`	—	—
`isEmpty_prod` 📖	mathematical	—	`IsEmpty`	—	—
`isEmpty_psigma` 📖	mathematical	—	`IsEmpty`	—	—
`isEmpty_psum` 📖	mathematical	—	`IsEmpty`	—	—
`isEmpty_sigma` 📖	mathematical	—	`IsEmpty`	—	—
`isEmpty_subtype` 📖	mathematical	—	`IsEmpty`	—	—
`isEmpty_sum` 📖	mathematical	—	`IsEmpty`	—	—
`isEmpty_ulift` 📖	mathematical	—	`IsEmpty`	—	—
`leftTotal_empty` 📖	mathematical	—	`Relator.LeftTotal`	—	—
`leftTotal_iff_isEmpty_left` 📖	mathematical	—	`Relator.LeftTotal` `IsEmpty`	—	—
`nonempty_fun` 📖	mathematical	—	`IsEmpty`	—	`not_iff_not` `not_nonempty_iff` `isEmpty_fun` `not_isEmpty_iff`
`not_isEmpty_iff` 📖	mathematical	—	`IsEmpty`	—	`not_iff_comm` `not_nonempty_iff`
`not_isEmpty_of_nonempty` 📖	mathematical	—	`IsEmpty`	—	`not_isEmpty_iff`
`not_nonempty_iff` 📖	mathematical	—	`IsEmpty`	—	—
`rightTotal_empty` 📖	mathematical	—	`Relator.RightTotal`	—	—
`rightTotal_iff_isEmpty_right` 📖	mathematical	—	`Relator.RightTotal` `IsEmpty`	—	—
`wellFounded_of_isEmpty` 📖	—	—	—	—	—

---

← Back to Index