Pi

📁 Source: Mathlib/Order/Interval/Set/Pi.lean

Statistics

Metric	Count
Definitions	0
Theorems Icc_diff_pi_univ_Ioc_subset, Icc_diff_pi_univ_Ioo_subset, disjoint_pi_univ_Ioc_update_left_right, image_mulSingle_Icc, image_mulSingle_Icc_left, image_mulSingle_Icc_right, image_mulSingle_Ico, image_mulSingle_Ico_left, image_mulSingle_Ico_right, image_mulSingle_Ioc, image_mulSingle_Ioc_left, image_mulSingle_Ioc_right, image_mulSingle_Ioo, image_mulSingle_Ioo_left, image_mulSingle_Ioo_right, image_mulSingle_uIcc, image_mulSingle_uIcc_left, image_mulSingle_uIcc_right, image_single_Icc, image_single_Icc_left, image_single_Icc_right, image_single_Ico, image_single_Ico_left, image_single_Ico_right, image_single_Ioc, image_single_Ioc_left, image_single_Ioc_right, image_single_Ioo, image_single_Ioo_left, image_single_Ioo_right, image_single_uIcc, image_single_uIcc_left, image_single_uIcc_right, image_update_Icc, image_update_Icc_left, image_update_Icc_right, image_update_Ico, image_update_Ico_left, image_update_Ico_right, image_update_Ioc, image_update_Ioc_left, image_update_Ioc_right, image_update_Ioo, image_update_Ioo_left, image_update_Ioo_right, image_update_uIcc, image_update_uIcc_left, image_update_uIcc_right, pi_univ_Icc, pi_univ_Ici, pi_univ_Ico_subset, pi_univ_Iic, pi_univ_Iio_subset, pi_univ_Ioc_subset, pi_univ_Ioc_update_left, pi_univ_Ioc_update_right, pi_univ_Ioc_update_union, pi_univ_Ioi_subset, pi_univ_Ioo_subset, pi_univ_uIcc, piecewise_mem_Icc, piecewise_mem_Icc'	62
Total	62

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_diff_pi_univ_Ioc_subset 📖	mathematical	—	Set instHasSubset instSDiff Icc Pi.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder pi univ Ioc iUnion Function.update	—	—
Icc_diff_pi_univ_Ioo_subset 📖	mathematical	—	Set instHasSubset instSDiff Icc Pi.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder pi univ Ioo instUnion iUnion Function.update	—	lt_or_ge
disjoint_pi_univ_Ioc_update_left_right 📖	mathematical	—	Disjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice pi univ Ioc Function.update	—	disjoint_left LE.le.not_gt mem_univ Function.update_self
image_mulSingle_Icc 📖	mathematical	—	image Pi.mulSingle Icc PartialOrder.toPreorder Pi.preorder	—	image_update_Icc
image_mulSingle_Icc_left 📖	mathematical	—	image Pi.mulSingle Icc PartialOrder.toPreorder Pi.preorder Pi.instOne	—	image_update_Icc_left
image_mulSingle_Icc_right 📖	mathematical	—	image Pi.mulSingle Icc PartialOrder.toPreorder Pi.preorder Pi.instOne	—	image_update_Icc_right
image_mulSingle_Ico 📖	mathematical	—	image Pi.mulSingle Ico PartialOrder.toPreorder Pi.preorder	—	image_update_Ico
image_mulSingle_Ico_left 📖	mathematical	—	image Pi.mulSingle Ico PartialOrder.toPreorder Pi.preorder Pi.instOne	—	image_update_Ico_left
image_mulSingle_Ico_right 📖	mathematical	—	image Pi.mulSingle Ico PartialOrder.toPreorder Pi.preorder Pi.instOne	—	image_update_Ico_right
image_mulSingle_Ioc 📖	mathematical	—	image Pi.mulSingle Ioc PartialOrder.toPreorder Pi.preorder	—	image_update_Ioc
image_mulSingle_Ioc_left 📖	mathematical	—	image Pi.mulSingle Ioc PartialOrder.toPreorder Pi.preorder Pi.instOne	—	image_update_Ioc_left
image_mulSingle_Ioc_right 📖	mathematical	—	image Pi.mulSingle Ioc PartialOrder.toPreorder Pi.preorder Pi.instOne	—	image_update_Ioc_right
image_mulSingle_Ioo 📖	mathematical	—	image Pi.mulSingle Ioo PartialOrder.toPreorder Pi.preorder	—	image_update_Ioo
image_mulSingle_Ioo_left 📖	mathematical	—	image Pi.mulSingle Ioo PartialOrder.toPreorder Pi.preorder Pi.instOne	—	image_update_Ioo_left
image_mulSingle_Ioo_right 📖	mathematical	—	image Pi.mulSingle Ioo PartialOrder.toPreorder Pi.preorder Pi.instOne	—	image_update_Ioo_right
image_mulSingle_uIcc 📖	mathematical	—	image Pi.mulSingle uIcc Pi.instLattice	—	image_update_uIcc
image_mulSingle_uIcc_left 📖	mathematical	—	image Pi.mulSingle uIcc Pi.instLattice Pi.instOne	—	image_update_uIcc_left
image_mulSingle_uIcc_right 📖	mathematical	—	image Pi.mulSingle uIcc Pi.instLattice Pi.instOne	—	image_update_uIcc_right
image_single_Icc 📖	mathematical	—	image Pi.single Icc PartialOrder.toPreorder Pi.preorder	—	image_update_Icc
image_single_Icc_left 📖	mathematical	—	image Pi.single Icc PartialOrder.toPreorder Pi.preorder Pi.instZero	—	image_update_Icc_left
image_single_Icc_right 📖	mathematical	—	image Pi.single Icc PartialOrder.toPreorder Pi.preorder Pi.instZero	—	image_update_Icc_right
image_single_Ico 📖	mathematical	—	image Pi.single Ico PartialOrder.toPreorder Pi.preorder	—	image_update_Ico
image_single_Ico_left 📖	mathematical	—	image Pi.single Ico PartialOrder.toPreorder Pi.preorder Pi.instZero	—	image_update_Ico_left
image_single_Ico_right 📖	mathematical	—	image Pi.single Ico PartialOrder.toPreorder Pi.preorder Pi.instZero	—	image_update_Ico_right
image_single_Ioc 📖	mathematical	—	image Pi.single Ioc PartialOrder.toPreorder Pi.preorder	—	image_update_Ioc
image_single_Ioc_left 📖	mathematical	—	image Pi.single Ioc PartialOrder.toPreorder Pi.preorder Pi.instZero	—	image_update_Ioc_left
image_single_Ioc_right 📖	mathematical	—	image Pi.single Ioc PartialOrder.toPreorder Pi.preorder Pi.instZero	—	image_update_Ioc_right
image_single_Ioo 📖	mathematical	—	image Pi.single Ioo PartialOrder.toPreorder Pi.preorder	—	image_update_Ioo
image_single_Ioo_left 📖	mathematical	—	image Pi.single Ioo PartialOrder.toPreorder Pi.preorder Pi.instZero	—	image_update_Ioo_left
image_single_Ioo_right 📖	mathematical	—	image Pi.single Ioo PartialOrder.toPreorder Pi.preorder Pi.instZero	—	image_update_Ioo_right
image_single_uIcc 📖	mathematical	—	image Pi.single uIcc Pi.instLattice	—	image_update_uIcc
image_single_uIcc_left 📖	mathematical	—	image Pi.single uIcc Pi.instLattice Pi.instZero	—	image_update_uIcc_left
image_single_uIcc_right 📖	mathematical	—	image Pi.single uIcc Pi.instLattice Pi.instZero	—	image_update_uIcc_right
image_update_Icc 📖	mathematical	—	image Function.update Icc PartialOrder.toPreorder Pi.preorder	—	ext pi_univ_Icc Function.update_self mem_univ eq_or_ne Function.update_of_ne
image_update_Icc_left 📖	mathematical	—	image Function.update Icc PartialOrder.toPreorder Pi.preorder	—	Function.update_eq_self image_update_Icc
image_update_Icc_right 📖	mathematical	—	image Function.update Icc PartialOrder.toPreorder Pi.preorder	—	Function.update_eq_self image_update_Icc
image_update_Ico 📖	mathematical	—	image Function.update Ico PartialOrder.toPreorder Pi.preorder	—	Icc_diff_right image_diff Function.update_injective image_singleton image_update_Icc
image_update_Ico_left 📖	mathematical	—	image Function.update Ico PartialOrder.toPreorder Pi.preorder	—	Function.update_eq_self image_update_Ico
image_update_Ico_right 📖	mathematical	—	image Function.update Ico PartialOrder.toPreorder Pi.preorder	—	Function.update_eq_self image_update_Ico
image_update_Ioc 📖	mathematical	—	image Function.update Ioc PartialOrder.toPreorder Pi.preorder	—	Icc_diff_left image_diff Function.update_injective image_singleton image_update_Icc
image_update_Ioc_left 📖	mathematical	—	image Function.update Ioc PartialOrder.toPreorder Pi.preorder	—	Function.update_eq_self image_update_Ioc
image_update_Ioc_right 📖	mathematical	—	image Function.update Ioc PartialOrder.toPreorder Pi.preorder	—	Function.update_eq_self image_update_Ioc
image_update_Ioo 📖	mathematical	—	image Function.update Ioo PartialOrder.toPreorder Pi.preorder	—	Ico_diff_left image_diff Function.update_injective image_singleton image_update_Ico
image_update_Ioo_left 📖	mathematical	—	image Function.update Ioo PartialOrder.toPreorder Pi.preorder	—	Function.update_eq_self image_update_Ioo
image_update_Ioo_right 📖	mathematical	—	image Function.update Ioo PartialOrder.toPreorder Pi.preorder	—	Function.update_eq_self image_update_Ioo
image_update_uIcc 📖	mathematical	—	image Function.update uIcc Pi.instLattice	—	image_update_Icc Function.update_sup Function.update_inf
image_update_uIcc_left 📖	mathematical	—	image Function.update uIcc Pi.instLattice	—	Function.update_eq_self image_update_uIcc
image_update_uIcc_right 📖	mathematical	—	image Function.update uIcc Pi.instLattice	—	Function.update_eq_self image_update_uIcc
pi_univ_Icc 📖	mathematical	—	pi univ Icc Pi.preorder	—	ext
pi_univ_Ici 📖	mathematical	—	pi univ Ici Pi.preorder	—	ext
pi_univ_Ico_subset 📖	mathematical	—	Set instHasSubset pi univ Ico Pi.preorder	—	pi_univ_Iio_subset
pi_univ_Iic 📖	mathematical	—	pi univ Iic Pi.preorder	—	ext
pi_univ_Iio_subset 📖	mathematical	—	Set instHasSubset pi univ Iio Pi.preorder	—	pi_univ_Ioi_subset
pi_univ_Ioc_subset 📖	mathematical	—	Set instHasSubset pi univ Ioc Pi.preorder	—	pi_univ_Ioi_subset
pi_univ_Ioc_update_left 📖	mathematical	Preorder.toLE	pi univ Ioc Function.update Set instInter setOf Preorder.toLT	—	Ioi_inter_Iic inter_assoc inter_eq_self_of_subset_left Ioi_subset_Ioi univ_pi_update pi_inter_compl singleton_pi'
pi_univ_Ioc_update_right 📖	mathematical	Preorder.toLE	pi univ Ioc Function.update Set instInter setOf	—	Ioi_inter_Iic inter_left_comm inter_eq_self_of_subset_left Iic_subset_Iic univ_pi_update pi_inter_compl singleton_pi'
pi_univ_Ioc_update_union 📖	mathematical	Set instMembership Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	instUnion pi univ Ioc Function.update	—	pi_univ_Ioc_update_left pi_univ_Ioc_update_right univ_inter
pi_univ_Ioi_subset 📖	mathematical	—	Set instHasSubset pi univ Ioi Pi.preorder	—	le_of_lt not_lt_of_ge
pi_univ_Ioo_subset 📖	mathematical	—	Set instHasSubset pi univ Ioo Pi.preorder	—	pi_univ_Ioi_subset pi_univ_Iio_subset
pi_univ_uIcc 📖	mathematical	—	pi univ uIcc Pi.instLattice	—	pi_univ_Icc
piecewise_mem_Icc 📖	mathematical	Set instMembership Icc	Pi.preorder piecewise	—	le_piecewise piecewise_le
piecewise_mem_Icc' 📖	mathematical	Set instMembership Icc Pi.preorder	piecewise	—	piecewise_mem_Icc

---

← Back to Index