Theorems · Theorem · logic and foundations
Set.piecewise_eqOn
∀ {α : Type u_1} {β : Type u_2} (s : Set α) [inst : (j : α) → Decidable (j ∈ s)] (f g : α → β),
Set.EqOn (s.piecewise f g) f s- Defined in
- Mathlib.Data.Set.Piecewise
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
- Assumes
- Decidable
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.EqOnstatement · cited by 603
- Set.piecewisestatement · cited by 136
- Set.piecewise_eq_of_memproof · cited by 49
Cited by6
Results whose statement or proof uses this declaration.
- MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaarproof · cited by 3
- Set.piecewise_range_compproof · cited by 2
- piecewise_ae_eq_restrictproof · cited by 2
- Set.injective_piecewise_iffproof · cited by 1
- ContinuousMap.isComplete_setOfPred_eqOnproof · cited by 1
- Set.MapsTo.piecewise_iteproof · cited by 0