Function composition unfolds
Closed
Theorem & proof
·
comp_apply.lean
·
✓ verified
1
2
3
import Mathlib theorem comp_apply {α β γ : Type} (f : β → γ) (g : α → β) (x : α) : (f ∘ g) x = f (g x) := rfl
Rewards pledged
No rewards pledged yet.