PSet

📁 Source: Mathlib/SetTheory/ZFC/PSet.lean

Statistics

Metric	Count
Definitions `PSet`, `Func`, `embed`, `empty`, `image`, `insert`, `instCoeSet`, `instEmptyCollection`, `instHasSSubset`, `instHasSubset`, `instInhabited`, `instInhabitedTypeInsert`, `instInsert`, `instMembership`, `instPreorder`, `instSep`, `instSingleton`, `instWellFoundedRelation`, `ofNat`, `omega`, `powerset`, `sUnion`, `sep`, `setoid`, `toSet`, `«term⋃₀_»`	26
Theorems `comm`, `eq`, `euc`, `exists_left`, `exists_right`, `ext`, `refl`, `rfl`, `trans`, `congr_left`, `congr_right`, `ext`, `mk`, `congr_left`, `congr_right`, `empty_def`, `empty_subset`, `equiv_empty`, `equiv_iff`, `equiv_iff_mem`, `equiv_of_isEmpty`, `eta`, `func_mem`, `instIsEmptyTypeEmptyCollection`, `instIsNonstrictStrictOrderSubsetSSubset`, `instIsTransSubset`, `instIsWellFoundedMem`, `instLawfulSingleton`, `instReflSubset`, `le_def`, `lift_mem_embed`, `lt_def`, `mem_asymm`, `mem_def`, `mem_image`, `mem_insert`, `mem_insert_iff`, `mem_insert_of_mem`, `mem_irrefl`, `mem_of_subset`, `mem_pair`, `mem_powerset`, `mem_sUnion`, `mem_sep`, `mem_singleton`, `mem_toSet`, `mem_wf`, `mk_func`, `mk_type`, `nonempty_def`, `nonempty_of_mem`, `nonempty_of_nonempty_type`, `nonempty_toSet_iff`, `nonempty_type_iff_nonempty`, `notMem_empty`, `notMem_of_subset`, `not_nonempty_empty`, `not_subset_of_mem`, `subset_iff`, `toSet_empty`, `toSet_sUnion`	61
Total	87

PSet

Definitions

Name	Category	Theorems
`Func` 📖	CompOp	8 math math: `Equiv.exists_left`, `mem_def`, `equiv_iff`, `func_mem`, `eta`, `ZFSet.sUnion_lem`, `Equiv.exists_right`, `mk_func`
`embed` 📖	CompOp	1 math math: `lift_mem_embed`
`empty` 📖	CompOp	—
`image` 📖	CompOp	1 math math: `mem_image`
`insert` 📖	CompOp	—
`instCoeSet` 📖	CompOp	—
`instEmptyCollection` 📖	CompOp	9 math math: `instIsEmptyTypeEmptyCollection`, `notMem_empty`, `instLawfulSingleton`, `rank_empty`, `toSet_empty`, `not_nonempty_empty`, `empty_subset`, `equiv_empty`, `empty_def`
`instHasSSubset` 📖	CompOp	2 math math: `instIsNonstrictStrictOrderSubsetSSubset`, `lt_def`
`instHasSubset` 📖	CompOp	12 math math: `instIsNonstrictStrictOrderSubsetSSubset`, `instReflSubset`, `Subset.congr_right`, `subset_iff`, `Subset.congr_left`, `Equiv.ext`, `mem_powerset`, `instIsTransSubset`, `ZFSet.subset_iff`, `not_subset_of_mem`, `empty_subset`, `le_def`
`instInhabited` 📖	CompOp	—
`instInhabitedTypeInsert` 📖	CompOp	—
`instInsert` 📖	CompOp	7 math math: `mem_insert_of_mem`, `rank_insert`, `instLawfulSingleton`, `mem_pair`, `mem_insert_iff`, `mem_insert`, `rank_pair`
`instMembership` 📖	CompOp	27 math math: `mem_wf`, `instIsWellFoundedMem`, `notMem_of_subset`, `mem_singleton`, `notMem_empty`, `rank_eq_wfRank`, `equiv_iff_mem`, `subset_iff`, `mem_sUnion`, `mem_def`, `nonempty_def`, `mem_powerset`, `Mem.mk`, `Ordinal.mem_toPSet_iff`, `mem_sep`, `Mem.congr_right`, `ZFSet.mk_mem_iff`, `func_mem`, `lift_mem_embed`, `mem_irrefl`, `lt_rank_iff`, `mem_pair`, `Mem.congr_left`, `mem_image`, `mem_toSet`, `mem_insert_iff`, `mem_insert`
`instPreorder` 📖	CompOp	2 math math: `lt_def`, `le_def`
`instSep` 📖	CompOp	—
`instSingleton` 📖	CompOp	5 math math: `mem_singleton`, `instLawfulSingleton`, `rank_singleton`, `mem_pair`, `rank_pair`
`instWellFoundedRelation` 📖	CompOp	—
`ofNat` 📖	CompOp	—
`omega` 📖	CompOp	—
`powerset` 📖	CompOp	2 math math: `mem_powerset`, `rank_powerset`
`sUnion` 📖	CompOp	5 math math: `le_succ_rank_sUnion`, `mem_sUnion`, `rank_sUnion_le`, `ZFSet.sUnion_lem`, `toSet_sUnion`
`sep` 📖	CompOp	1 math math: `mem_sep`
`setoid` 📖	CompOp	2 math math: `ZFSet.mk_eq`, `ZFSet.mk_out`
`toSet` 📖	CompOp	5 math math: `toSet_empty`, `Equiv.eq`, `toSet_sUnion`, `nonempty_toSet_iff`, `mem_toSet`
`«term⋃₀_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`empty_def` 📖	mathematical	—	`PSet` `instEmptyCollection`	—	—
`empty_subset` 📖	mathematical	—	`PSet` `instHasSubset` `instEmptyCollection`	—	—
`equiv_empty` 📖	mathematical	—	`Equiv` `PSet` `instEmptyCollection`	—	`equiv_of_isEmpty` `instIsEmptyTypeEmptyCollection`
`equiv_iff` 📖	mathematical	—	`Equiv` `Func`	—	—
`equiv_iff_mem` 📖	mathematical	—	`Equiv` `PSet` `instMembership`	—	`Mem.congr_right` `Equiv.symm`
`equiv_of_isEmpty` 📖	mathematical	—	`Equiv`	—	`equiv_iff`
`eta` 📖	mathematical	—	`Type` `Func`	—	—
`func_mem` 📖	mathematical	—	`PSet` `instMembership` `Func`	—	—
`instIsEmptyTypeEmptyCollection` 📖	mathematical	—	`IsEmpty` `Type` `PSet` `instEmptyCollection`	—	—
`instIsNonstrictStrictOrderSubsetSSubset` 📖	mathematical	—	`IsNonstrictStrictOrder` `PSet` `instHasSubset` `instHasSSubset`	—	—
`instIsTransSubset` 📖	mathematical	—	`IsTrans` `PSet` `instHasSubset`	—	`Equiv.trans`
`instIsWellFoundedMem` 📖	mathematical	—	`IsWellFounded` `PSet` `instMembership`	—	`mem_wf`
`instLawfulSingleton` 📖	mathematical	—	`PSet` `instEmptyCollection` `instInsert` `instSingleton`	—	—
`instReflSubset` 📖	mathematical	—	`PSet` `instHasSubset`	—	`Equiv.refl`
`le_def` 📖	mathematical	—	`PSet` `Preorder.toLE` `instPreorder` `instHasSubset`	—	—
`lift_mem_embed` 📖	mathematical	—	`PSet` `instMembership` `embed` `Lift`	—	`Equiv.rfl`
`lt_def` 📖	mathematical	—	`PSet` `Preorder.toLT` `instPreorder` `instHasSSubset`	—	—
`mem_asymm` 📖	—	`PSet` `instMembership`	—	—	`asymm_of` `instAsymmOfIsWellFounded` `instIsWellFoundedMem`
`mem_def` 📖	mathematical	—	`PSet` `instMembership` `Equiv` `Func`	—	—
`mem_image` 📖	mathematical	`Equiv`	`PSet` `instMembership` `image`	—	`Equiv.trans`
`mem_insert` 📖	mathematical	—	`PSet` `instMembership` `instInsert`	—	`mem_insert_iff` `Equiv.rfl`
`mem_insert_iff` 📖	mathematical	—	`PSet` `instMembership` `instInsert` `Equiv`	—	—
`mem_insert_of_mem` 📖	mathematical	`PSet` `instMembership`	`instInsert`	—	`mem_insert_iff`
`mem_irrefl` 📖	mathematical	—	`PSet` `instMembership`	—	`irrefl_of` `instAsymmOfIsWellFounded` `instIsWellFoundedMem`
`mem_of_subset` 📖	—	`PSet` `instHasSubset` `instMembership`	—	—	`Equiv.trans`
`mem_pair` 📖	mathematical	—	`PSet` `instMembership` `instInsert` `instSingleton` `Equiv`	—	—
`mem_powerset` 📖	mathematical	—	`PSet` `instMembership` `powerset` `instHasSubset`	—	`Subset.congr_left` `Equiv.refl`
`mem_sUnion` 📖	mathematical	—	`PSet` `instMembership` `sUnion`	—	`Mem.congr_left` `eta` `Equiv.trans`
`mem_sep` 📖	mathematical	—	`PSet` `instMembership` `sep`	—	`Equiv.symm`
`mem_singleton` 📖	mathematical	—	`PSet` `instMembership` `instSingleton` `Equiv`	—	`mem_insert_iff` `notMem_empty`
`mem_toSet` 📖	mathematical	—	`PSet` `Set` `Set.instMembership` `toSet` `instMembership`	—	—
`mem_wf` 📖	mathematical	—	`PSet` `instMembership`	—	`Equiv.refl`
`mk_func` 📖	mathematical	—	`Func`	—	—
`mk_type` 📖	mathematical	—	`Type`	—	—
`nonempty_def` 📖	mathematical	—	`Nonempty` `PSet` `instMembership`	—	—
`nonempty_of_mem` 📖	mathematical	`PSet` `instMembership`	`Nonempty`	—	—
`nonempty_of_nonempty_type` 📖	mathematical	—	`Nonempty`	—	`nonempty_type_iff_nonempty`
`nonempty_toSet_iff` 📖	mathematical	—	`Set.Nonempty` `PSet` `toSet` `Nonempty`	—	—
`nonempty_type_iff_nonempty` 📖	mathematical	—	`Type` `Nonempty`	—	`func_mem`
`notMem_empty` 📖	mathematical	—	`PSet` `instMembership` `instEmptyCollection`	—	`IsEmpty.exists_iff` `instIsEmptyTypeEmptyCollection`
`notMem_of_subset` 📖	mathematical	`PSet` `instHasSubset`	`instMembership`	—	`not_subset_of_mem`
`not_nonempty_empty` 📖	mathematical	—	`Nonempty` `PSet` `instEmptyCollection`	—	`toSet_empty`
`not_subset_of_mem` 📖	mathematical	`PSet` `instMembership`	`instHasSubset`	—	`mem_irrefl` `mem_of_subset`
`subset_iff` 📖	mathematical	—	`PSet` `instHasSubset` `instMembership`	—	`mem_of_subset`
`toSet_empty` 📖	mathematical	—	`toSet` `PSet` `instEmptyCollection` `Set` `Set.instEmptyCollection`	—	—
`toSet_sUnion` 📖	mathematical	—	`toSet` `sUnion` `Set.sUnion` `PSet` `Set.image` `Set`	—	`Set.ext` `Set.sUnion_image` `Set.iUnion_congr_Prop`

PSet.Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm` 📖	mathematical	—	`PSet.Equiv`	—	`symm`
`eq` 📖	mathematical	—	`PSet.Equiv` `PSet.toSet`	—	`PSet.equiv_iff_mem` `Set.ext_iff`
`euc` 📖	—	`PSet.Equiv`	—	—	—
`exists_left` 📖	mathematical	`PSet.Equiv`	`PSet.Func`	—	`PSet.equiv_iff`
`exists_right` 📖	mathematical	`PSet.Equiv`	`PSet.Func`	—	`PSet.equiv_iff`
`ext` 📖	mathematical	—	`PSet.Equiv` `PSet` `PSet.instHasSubset`	—	`symm`
`refl` 📖	mathematical	—	`PSet.Equiv`	—	—
`rfl` 📖	mathematical	—	`PSet.Equiv`	—	`refl`
`trans` 📖	—	`PSet.Equiv`	—	—	`euc` `symm`

PSet.Mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_left` 📖	mathematical	`PSet.Equiv`	`PSet` `PSet.instMembership`	—	`PSet.Equiv.trans` `PSet.Equiv.symm`
`congr_right` 📖	mathematical	`PSet.Equiv`	`PSet` `PSet.instMembership`	—	`PSet.Equiv.trans` `PSet.Equiv.euc`
`ext` 📖	mathematical	`PSet` `PSet.instMembership`	`PSet.Equiv`	—	`PSet.Equiv.symm`
`mk` 📖	mathematical	—	`PSet` `PSet.instMembership`	—	`PSet.Equiv.refl`

PSet.Subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_left` 📖	mathematical	`PSet.Equiv`	`PSet` `PSet.instHasSubset`	—	`PSet.Equiv.trans` `PSet.Equiv.symm`
`congr_right` 📖	mathematical	`PSet.Equiv`	`PSet` `PSet.instHasSubset`	—	`PSet.Equiv.trans` `PSet.Equiv.symm`

(root)

Definitions

Name	Category	Theorems
`PSet` 📖	CompData	50 math math: `ZFSet.mk_eq`, `PSet.instIsEmptyTypeEmptyCollection`, `PSet.mem_wf`, `PSet.instIsWellFoundedMem`, `PSet.instIsNonstrictStrictOrderSubsetSSubset`, `PSet.instReflSubset`, `PSet.mem_singleton`, `PSet.notMem_empty`, `PSet.rank_eq_wfRank`, `ZFSet.mk_out`, `PSet.equiv_iff_mem`, `PSet.Subset.congr_right`, `PSet.rank_insert`, `PSet.subset_iff`, `PSet.mem_sUnion`, `PSet.Subset.congr_left`, `PSet.mem_def`, `PSet.Equiv.ext`, `PSet.instLawfulSingleton`, `PSet.nonempty_def`, `PSet.mem_powerset`, `PSet.Mem.mk`, `PSet.instIsTransSubset`, `Ordinal.mem_toPSet_iff`, `PSet.mem_sep`, `PSet.Mem.congr_right`, `PSet.rank_empty`, `ZFSet.mk_mem_iff`, `PSet.func_mem`, `ZFSet.subset_iff`, `PSet.lift_mem_embed`, `PSet.toSet_empty`, `PSet.mem_irrefl`, `PSet.rank_singleton`, `PSet.not_nonempty_empty`, `PSet.empty_subset`, `PSet.equiv_empty`, `PSet.lt_rank_iff`, `PSet.mem_pair`, `PSet.toSet_sUnion`, `PSet.lt_def`, `PSet.Mem.congr_left`, `PSet.le_def`, `PSet.nonempty_toSet_iff`, `PSet.mem_image`, `PSet.mem_toSet`, `PSet.mem_insert_iff`, `PSet.mem_insert`, `PSet.rank_pair`, `PSet.empty_def`

---

← Back to Index