Skip to content

Commit

Permalink
chore: deprecate alias Function.funext_iff in favor of funext_iff (
Browse files Browse the repository at this point in the history
  • Loading branch information
jcommelin authored Oct 17, 2024
1 parent cc0bc87 commit c521f01
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions Batteries/Logic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@ theorem funext₃ {β : α → Sort _} {γ : ∀ a, β a → Sort _} {δ : ∀ a
{f g : ∀ a b c, δ a b c} (h : ∀ a b c, f a b c = g a b c) : f = g :=
funext fun _ => funext₂ <| h _

@[deprecated (since := "2024-10-17")]
protected alias Function.funext_iff := funext_iff

theorem ne_of_apply_ne {α β : Sort _} (f : α → β) {x y : α} : f x ≠ f y → x ≠ y :=
Expand Down

0 comments on commit c521f01

Please sign in to comment.