diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean index d56317c28..e98ca6848 100644 --- a/library/data/finset/basic.lean +++ b/library/data/finset/basic.lean @@ -453,7 +453,7 @@ quot.lift_on₂ s₁ s₂ (λ s₁ a i, mem_perm p₂ (s₁ a (mem_perm (perm.symm p₁) i))) (λ s₂ a i, mem_perm (perm.symm p₂) (s₂ a (mem_perm p₁ i))))) -infix `⊆`:50 := subset +infix `⊆` := subset theorem empty_subset (s : finset A) : ∅ ⊆ s := quot.induction_on s (λ l, list.nil_sub (elt_of l)) diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 9cbecdf3c..dc9fcc9ae 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -286,7 +286,7 @@ assume nin nainl, absurd (or.inr nainl) nin definition sublist (l₁ l₂ : list T) := ∀ ⦃a : T⦄, a ∈ l₁ → a ∈ l₂ -infix `⊆`:50 := sublist +infix `⊆` := sublist theorem nil_sub (l : list T) : [] ⊆ l := λ b i, false.elim (iff.mp (mem_nil_iff b) i) diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index 4cf2d7104..3b421346c 100644 --- a/library/data/set/basic.lean +++ b/library/data/set/basic.lean @@ -22,7 +22,7 @@ theorem setext {a b : set X} (H : ∀x, x ∈ a ↔ x ∈ b) : a = b := funext (take x, propext (H x)) definition subset (a b : set X) := ∀⦃x⦄, x ∈ a → x ∈ b -infix `⊆`:50 := subset +infix `⊆` := subset /- bounded quantification -/ diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index f1233051f..7ed4ce1ae 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -88,6 +88,7 @@ reserve infix `∈`:50 reserve infix `∉`:50 reserve infixl `∩`:70 reserve infixl `∪`:65 +reserve infix `⊆`:50 /- other symbols -/