Skip to content

Commit

Permalink
Update Mathlib/Logic/Relation.lean
Browse files Browse the repository at this point in the history
Co-authored-by: Eric Wieser <[email protected]>
  • Loading branch information
urkud and eric-wieser authored Feb 26, 2025
1 parent 81721a4 commit fd7af8b
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Logic/Relation.lean
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,7 @@ theorem comp_eq_fun (f : γ → β) : r ∘r (· = f ·) = (r · <| f ·) := by
theorem comp_eq : r ∘r (· = ·) = r := comp_eq_fun ..

@[simp]
theorem fun_eq_comp (f : γ → α) : (f · = ·) ∘r r = (f · |> r <| ·) := by
theorem fun_eq_comp (f : γ → α) : (f · = ·) ∘r r = (r <| f ·) := by
ext x y
simp [Comp]

Expand Down

0 comments on commit fd7af8b

Please sign in to comment.