Piecewise

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

Statistics

Metric	Count
Definitions	0
Theorems `piecewise_ite`, `piecewise_ite'`, `piecewise_ite`, `apply_piecewise`, `apply_piecewise₂`, `eqOn_piecewise`, `injective_piecewise_iff`, `le_piecewise`, `pi_piecewise`, `piecewise_comp`, `piecewise_compl`, `piecewise_empty`, `piecewise_eqOn`, `piecewise_eqOn_compl`, `piecewise_eq_of_mem`, `piecewise_eq_of_notMem`, `piecewise_insert`, `piecewise_insert_of_ne`, `piecewise_insert_self`, `piecewise_le`, `piecewise_mem_pi`, `piecewise_mono`, `piecewise_op`, `piecewise_op₂`, `piecewise_preimage`, `piecewise_range_comp`, `piecewise_same`, `piecewise_singleton`, `piecewise_univ`, `range_piecewise`, `univ_pi_piecewise`, `univ_pi_piecewise_univ`	32
Total	32

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_piecewise` 📖	mathematical	—	`piecewise`	—	`piecewise_eq_of_mem` `piecewise_eq_of_notMem`
`apply_piecewise₂` 📖	mathematical	—	`piecewise`	—	`piecewise_eq_of_mem` `piecewise_eq_of_notMem`
`eqOn_piecewise` 📖	mathematical	—	`EqOn` `piecewise` `Set` `instInter` `Compl.compl` `instCompl`	—	`piecewise_eq_of_mem` `instIsEmptyFalse` `piecewise_eq_of_notMem`
`injective_piecewise_iff` 📖	mathematical	—	`piecewise` `InjOn` `Compl.compl` `Set` `instCompl`	—	`injOn_univ` `union_compl_self` `injOn_union` `disjoint_compl_right` `EqOn.injOn_iff` `piecewise_eqOn` `piecewise_eqOn_compl` `piecewise_eq_of_mem` `piecewise_eq_of_notMem`
`le_piecewise` 📖	mathematical	`Preorder.toLE`	`Pi.hasLe` `piecewise`	—	`piecewise_le`
`pi_piecewise` 📖	mathematical	—	`pi` `piecewise` `Set` `instInter` `instSDiff`	—	`pi_if`
`piecewise_comp` 📖	mathematical	—	`piecewise` `preimage` `Set` `instMembership`	—	—
`piecewise_compl` 📖	mathematical	—	`piecewise` `Compl.compl` `Set` `instCompl`	—	`piecewise_eq_of_notMem` `piecewise_eq_of_mem`
`piecewise_empty` 📖	mathematical	—	`piecewise` `Set` `instEmptyCollection`	—	—
`piecewise_eqOn` 📖	mathematical	—	`EqOn` `piecewise`	—	`piecewise_eq_of_mem`
`piecewise_eqOn_compl` 📖	mathematical	—	`EqOn` `piecewise` `Compl.compl` `Set` `instCompl`	—	`piecewise_eq_of_notMem`
`piecewise_eq_of_mem` 📖	mathematical	`Set` `instMembership`	`piecewise`	—	—
`piecewise_eq_of_notMem` 📖	mathematical	`Set` `instMembership`	`piecewise`	—	—
`piecewise_insert` 📖	mathematical	—	`piecewise` `Set` `instInsert` `Function.update`	—	`Function.update_self` `Function.update_of_ne`
`piecewise_insert_of_ne` 📖	mathematical	—	`piecewise` `Set` `instInsert`	—	—
`piecewise_insert_self` 📖	mathematical	—	`piecewise` `Set` `instInsert`	—	—
`piecewise_le` 📖	mathematical	`Preorder.toLE`	`Pi.hasLe` `piecewise`	—	`piecewise_eq_of_mem` `piecewise_eq_of_notMem`
`piecewise_mem_pi` 📖	mathematical	`Set` `instMembership` `pi`	`piecewise`	—	`piecewise_eq_of_mem` `piecewise_eq_of_notMem`
`piecewise_mono` 📖	mathematical	`Preorder.toLE`	`Pi.hasLe` `piecewise`	—	`piecewise_le` `piecewise_eq_of_mem` `piecewise_eq_of_notMem`
`piecewise_op` 📖	mathematical	—	`piecewise`	—	`apply_piecewise`
`piecewise_op₂` 📖	mathematical	—	`piecewise`	—	`apply_piecewise₂`
`piecewise_preimage` 📖	mathematical	—	`preimage` `piecewise` `ite`	—	`ext` `piecewise_eq_of_mem` `piecewise_eq_of_notMem`
`piecewise_range_comp` 📖	mathematical	—	`piecewise` `range`	—	`EqOn.comp_eq` `piecewise_eqOn`
`piecewise_same` 📖	mathematical	—	`piecewise`	—	`piecewise_eq_of_mem` `piecewise_eq_of_notMem`
`piecewise_singleton` 📖	mathematical	—	`piecewise` `Set` `instSingletonSet` `Function.update`	—	`piecewise_eq_of_mem` `Function.update_self` `piecewise_eq_of_notMem` `Function.update_of_ne`
`piecewise_univ` 📖	mathematical	—	`piecewise` `univ`	—	—
`range_piecewise` 📖	mathematical	—	`range` `piecewise` `Set` `instUnion` `image` `Compl.compl` `instCompl`	—	`ext` `piecewise_eq_of_mem` `piecewise_eq_of_notMem`
`univ_pi_piecewise` 📖	mathematical	—	`pi` `univ` `piecewise` `Set` `instInter` `Compl.compl` `instCompl`	—	`pi_piecewise` `univ_inter` `compl_eq_univ_diff`
`univ_pi_piecewise_univ` 📖	mathematical	—	`pi` `univ` `piecewise` `Set`	—	`pi_piecewise` `univ_inter` `pi_univ` `inter_univ`

Set.EqOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`piecewise_ite` 📖	mathematical	`Set.EqOn`	`Set.piecewise` `Set.ite`	—	`piecewise_ite'` `mono` `Set.inter_subset_left`
`piecewise_ite'` 📖	mathematical	`Set.EqOn` `Set` `Set.instInter` `Compl.compl` `Set.instCompl`	`Set.piecewise` `Set.ite`	—	`Set.ite_inter_self` `Set.ite_inter_compl_self`

Set.MapsTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`piecewise_ite` 📖	mathematical	`Set.MapsTo` `Set` `Set.instInter` `Compl.compl` `Set.instCompl`	`Set.piecewise` `Set.ite`	—	`union_union` `congr` `Set.EqOn.mono` `Set.inter_subset_right` `Set.EqOn.symm` `Set.piecewise_eqOn` `Set.piecewise_eqOn_compl`

---

← Back to Index