Commit 2021-05-21 00:33 19247422

feat(data/set/basic): allow dot notation for trans and antisymm (#7681) Allow to write

example {α : Type*} {a b c : set α} (h : a ⊆ b)  (h': b ⊆ c) : a ⊆ c :=
h.trans h'
example {α : Type*} {a b : set α} (h : a ⊆ b)  (h': b ⊆ a) : 
  a = b := h.antisymm h'
example {α : Type*} {a b c : finset α} (h : a ⊆ b)  (h': b ⊆ c) : a ⊆ c :=
h.trans h'
example {α : Type*} {a b : finset α} (h : a ⊆ b)  (h': b ⊆ a) : a = b :=
h.antisymm h'