Piecewise

📁 Source: Mathlib/Data/Finset/Piecewise.lean

Statistics

Metric	Count
Definitions piecewise	1
Theorems le_piecewise_of_le_of_le, piecewise_cases, piecewise_coe, piecewise_compl, piecewise_congr, piecewise_empty, piecewise_eq_of_mem, piecewise_eq_of_notMem, piecewise_erase_univ, piecewise_idem_left, piecewise_idem_right, piecewise_insert, piecewise_insert_of_ne, piecewise_insert_self, piecewise_le_of_le_of_le, piecewise_le_piecewise, piecewise_le_piecewise', piecewise_mem_Icc, piecewise_mem_Icc', piecewise_mem_Icc_of_mem_of_mem, piecewise_mem_set_pi, piecewise_piecewise_of_subset_left, piecewise_piecewise_of_subset_right, piecewise_same, piecewise_singleton, piecewise_univ, update_eq_piecewise, update_piecewise, update_piecewise_of_mem, update_piecewise_of_notMem	30
Total	31

Finset

Definitions

Name	Category	Theorems
piecewise 📖	CompOp	52 math math: MultilinearMap.map_piecewise_smul, ContinuousMultilinearMap.map_piecewise_smul, piecewise_insert, FormalMultilinearSeries.changeOriginSeriesTerm_apply, piecewise_piecewise_of_subset_left, MultilinearMap.map_piecewise_sub_map_piecewise, sum_piecewise, piecewise_mem_Icc', ContinuousAlternatingMap.map_piecewise_smul, MultilinearMap.curryFinFinset_symm_apply_piecewise_const, ContinuousMultilinearMap.map_piecewise_add, piecewise_compl, update_eq_piecewise, piecewise_le_piecewise', ContinuousMultilinearMap.map_add_univ, MultilinearMap.map_add_sub_map_add_sub_linearDeriv, ContinuousMultilinearMap.curryFinFinset_apply_const, piecewise_cases, MultilinearMap.curryFinFinset_apply_const, MultilinearMap.map_add_eq_map_add_linearDeriv_add, ContinuousAlternatingMap.map_add_univ, ContinuousMultilinearMap.curryFinFinset_symm_apply_piecewise_const, MultilinearMap.map_piecewise_add, piecewise_le_of_le_of_le, update_piecewise_of_notMem, piecewise_insert_of_ne, piecewise_idem_right, piecewise_univ, piecewise_singleton, update_piecewise, le_piecewise_of_le_of_le, exists_finset_piecewise_mem_of_mem_nhds, piecewise_mem_Icc_of_mem_of_mem, piecewise_erase_univ, ContinuousAlternatingMap.map_piecewise_add, piecewise_mem_Icc, piecewise_same, piecewise_piecewise_of_subset_right, piecewise_empty, piecewise_idem_left, MultilinearMap.map_sub_map_piecewise, piecewise_eq_of_mem, piecewise_eq_of_notMem, FormalMultilinearSeries.changeOriginSeriesTerm_changeOriginIndexEquiv_symm, piecewise_le_piecewise, prod_piecewise, update_piecewise_of_mem, piecewise_insert_self, piecewise_mem_set_pi, piecewise_coe, MultilinearMap.map_add_univ, piecewise_congr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_piecewise_of_le_of_le 📖	mathematical	Pi.hasLe Preorder.toLE	piecewise	—	piecewise_cases
piecewise_cases 📖	mathematical	—	piecewise	—	piecewise_eq_of_mem piecewise_eq_of_notMem
piecewise_coe 📖	mathematical	—	Set.piecewise SetLike.coe Finset instSetLike piecewise	—	—
piecewise_compl 📖	mathematical	—	piecewise Compl.compl Finset BooleanAlgebra.toCompl booleanAlgebra	—	—
piecewise_congr 📖	mathematical	—	piecewise	—	if_ctx_congr
piecewise_empty 📖	mathematical	—	piecewise Finset instEmptyCollection	—	—
piecewise_eq_of_mem 📖	mathematical	Finset instMembership	piecewise	—	—
piecewise_eq_of_notMem 📖	mathematical	Finset instMembership	piecewise	—	—
piecewise_erase_univ 📖	mathematical	—	piecewise erase univ decidableMem Function.update	—	compl_singleton piecewise_compl piecewise_singleton
piecewise_idem_left 📖	mathematical	—	piecewise	—	piecewise_piecewise_of_subset_left Subset.refl
piecewise_idem_right 📖	mathematical	—	piecewise	—	piecewise_piecewise_of_subset_right Subset.refl
piecewise_insert 📖	mathematical	—	piecewise Finset instInsert Function.update	—	coe_insert
piecewise_insert_of_ne 📖	mathematical	—	piecewise Finset instInsert	—	—
piecewise_insert_self 📖	mathematical	—	piecewise Finset instInsert	—	—
piecewise_le_of_le_of_le 📖	mathematical	Pi.hasLe Preorder.toLE	piecewise	—	piecewise_cases
piecewise_le_piecewise 📖	mathematical	Pi.hasLe Preorder.toLE	piecewise	—	piecewise_le_piecewise'
piecewise_le_piecewise' 📖	mathematical	Preorder.toLE	Pi.hasLe piecewise	—	piecewise_eq_of_mem piecewise_eq_of_notMem
piecewise_mem_Icc 📖	mathematical	Pi.hasLe Preorder.toLE	Set Set.instMembership Set.Icc Pi.preorder piecewise	—	piecewise_mem_Icc_of_mem_of_mem Set.left_mem_Icc Set.right_mem_Icc
piecewise_mem_Icc' 📖	mathematical	Pi.hasLe Preorder.toLE	Set Set.instMembership Set.Icc Pi.preorder piecewise	—	piecewise_mem_Icc_of_mem_of_mem Set.right_mem_Icc Set.left_mem_Icc
piecewise_mem_Icc_of_mem_of_mem 📖	mathematical	Set Set.instMembership Set.Icc Pi.preorder	piecewise	—	le_piecewise_of_le_of_le piecewise_le_of_le_of_le
piecewise_mem_set_pi 📖	mathematical	Set Set.instMembership Set.pi	piecewise	—	piecewise_coe Set.piecewise_mem_pi
piecewise_piecewise_of_subset_left 📖	mathematical	Finset instHasSubset	piecewise	—	piecewise_congr piecewise_eq_of_mem
piecewise_piecewise_of_subset_right 📖	mathematical	Finset instHasSubset	piecewise	—	piecewise_congr piecewise_eq_of_notMem
piecewise_same 📖	mathematical	—	piecewise	—	piecewise_eq_of_mem piecewise_eq_of_notMem
piecewise_singleton 📖	mathematical	—	piecewise Finset instSingleton decidableMem Function.update	—	instLawfulSingleton piecewise_insert piecewise_empty
piecewise_univ 📖	mathematical	—	piecewise univ	—	—
update_eq_piecewise 📖	mathematical	—	Function.update piecewise Finset instSingleton decidableMem	—	piecewise_singleton
update_piecewise 📖	mathematical	—	Function.update piecewise	—	em Function.update_self piecewise_eq_of_mem piecewise_eq_of_notMem Function.update_of_ne
update_piecewise_of_mem 📖	mathematical	Finset instMembership	Function.update piecewise	—	update_piecewise piecewise_congr Function.update_of_ne
update_piecewise_of_notMem 📖	mathematical	Finset instMembership	Function.update piecewise	—	update_piecewise piecewise_congr Function.update_of_ne

---

← Back to Index