fix(data/set/basic): Fix set.lt_iff_ssubset. (#17047)

leanprover-community · Oct 18, 2022 · 8c9b005 · 8c9b005
1 parent 4af7699
commit 8c9b005
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
@@ -106,7 +106,7 @@ instance : has_inter (set α) := ⟨(⊓)⟩
 @[simp] lemma lt_eq_ssubset : ((<) : set α → set α → Prop) = (⊂) := rfl
 
 lemma le_iff_subset : s ≤ t ↔ s ⊆ t := iff.rfl
-lemma lt_iff_ssubset : s ≤ t ↔ s ⊆ t := iff.rfl
+lemma lt_iff_ssubset : s < t ↔ s ⊂ t := iff.rfl
 
 alias le_iff_subset ↔ _root_.has_le.le.subset _root_.has_subset.subset.le
 alias lt_iff_ssubset ↔ _root_.has_lt.lt.ssubset _root_.has_ssubset.ssubset.lt