Theorems · Theorem
Sum.update_inr_comp_inr
∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq β] [inst_1 : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i : β}
{x : γ}, Function.update f (Sum.inr i) x ∘ Sum.inr = Function.update (f ∘ Sum.inr) i x- Defined in
- Mathlib.Data.Sum.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Function.updatestatement · cited by 502
- Sum.inr_injectiveproof · cited by 40
- Function.update_comp_eq_of_injectiveproof · cited by 5
Cited by1
Results whose statement or proof uses this declaration.
- Sum.update_inr_apply_inrproof · cited by 0