Skip to content

Commit bacc8b0

Browse files
author
sven-manthe
committed
chore: fix name "Set.cou_inter_self_right_eq_coe" (#18222)
The old name contained a typo. The new one is symmetric to the name of the following lemma in the same file.
1 parent cf1c5c2 commit bacc8b0

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

Mathlib/Data/Set/Subset.lean

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -112,8 +112,10 @@ lemma image_val_union_self_left_eq : ↑D ∪ A = A :=
112112
union_eq_right.2 image_val_subset
113113

114114
@[simp]
115-
lemma cou_inter_self_right_eq_coe : A ∩ ↑D = ↑D :=
115+
lemma image_val_inter_self_right_eq_coe : A ∩ ↑D = ↑D :=
116116
inter_eq_right.2 image_val_subset
117+
@[deprecated (since := "2024-10-25")]
118+
alias cou_inter_self_right_eq_coe := image_val_inter_self_right_eq_coe
117119

118120
@[simp]
119121
lemma image_val_inter_self_left_eq_coe : ↑D ∩ A = ↑D :=

0 commit comments

Comments
 (0)