Zorn

📁 Source: Mathlib/Order/Zorn.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_mem, exists_mem_mem, instNonempty, exists_maxChain, exists_subset_flag, exists_maximal_of_chains_bounded, exists_maximal_of_nonempty_chains_bounded, zorn_le, zorn_le_nonempty, zorn_le_nonempty_Ici₀, zorn_le_nonempty₀, zorn_le₀, zorn_subset, zorn_subset_nonempty, zorn_superset, zorn_superset_nonempty	16
Total	16

Flag

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_mem 📖	mathematical	—	Flag Preorder.toLE SetLike.instMembership instSetLike	—	IsChain.exists_subset_flag Set.Subsingleton.isChain Set.subsingleton_singleton
exists_mem_mem 📖	mathematical	Preorder.toLE	Flag SetLike.instMembership instSetLike	—	IsChain.exists_subset_flag IsChain.pair
instNonempty 📖	mathematical	—	Flag Preorder.toLE	—	maxChain_spec

IsChain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_maxChain 📖	mathematical	IsChain	IsMaxChain Set Set.instHasSubset	—	zorn_subset_nonempty Set.mem_sUnion_of_mem eq_or_ne Set.subset_sUnion_of_mem Set.Subset.rfl Maximal.prop Maximal.eq_of_subset HasSubset.Subset.trans Set.instIsTransSubset
exists_subset_flag 📖	mathematical	IsChain Preorder.toLE	Set Set.instHasSubset SetLike.coe Flag Flag.instSetLike	—	exists_maxChain

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_maximal_of_chains_bounded 📖	—	—	—	—	maxChain_spec IsChain.insert Set.subset_insert Set.mem_insert
exists_maximal_of_nonempty_chains_bounded 📖	—	—	—	—	exists_maximal_of_chains_bounded Set.eq_empty_or_nonempty
zorn_le 📖	mathematical	BddAbove Preorder.toLE	IsMax	—	exists_maximal_of_chains_bounded le_trans
zorn_le_nonempty 📖	mathematical	BddAbove Preorder.toLE	IsMax	—	exists_maximal_of_nonempty_chains_bounded le_trans
zorn_le_nonempty_Ici₀ 📖	mathematical	Preorder.toLE	IsMax	—	zorn_le_nonempty₀ LE.le.trans
zorn_le_nonempty₀ 📖	mathematical	Set Set.instMembership Preorder.toLE	Maximal	—	zorn_le₀ Set.eq_empty_or_nonempty le_rfl LE.le.trans
zorn_le₀ 📖	mathematical	Set Set.instMembership Preorder.toLE	Maximal	—	zorn_le
zorn_subset 📖	mathematical	Set Set.instMembership Set.instHasSubset	Maximal Set.instLE	—	zorn_le₀
zorn_subset_nonempty 📖	mathematical	Set Set.instMembership Set.instHasSubset	Maximal Set.instLE	—	zorn_le_nonempty₀
zorn_superset 📖	mathematical	Set Set.instMembership Set.instHasSubset	Minimal Set.instLE	—	zorn_le₀ IsChain.symm
zorn_superset_nonempty 📖	mathematical	Set Set.instMembership Set.instHasSubset	Minimal Set.instLE	—	zorn_le_nonempty₀ IsChain.symm

---

← Back to Index