Zulip Chat Archive

Stream: general

Topic: missing transitivity tags


view this post on Zulip Johan Commelin (Aug 05 2019 at 14:54):

Should all of these be tagged with @[trans]? Or is there a reason to only do that for sets?

git grep "subset.trans" | grep theorem
src/data/finset.lean:theorem subset.trans {s₁ s₂ s₃ : finset α} : s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃ := subset.trans
src/data/multiset.lean:theorem subset.trans {s t u : multiset α} : s ⊆ t → t ⊆ u → s ⊆ u :=
src/data/set/basic.lean:@[trans] theorem subset.trans {a b c : set α} (ab : a ⊆ b) (bc : b ⊆ c) : a ⊆ c :=
src/set_theory/lists.lean:theorem subset.trans {l₁ l₂ l₃ : lists' α tt}

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 15:45):

This takes us back to Chris' point. If we just used le and make them partial orders then le_trans would kick in.


Last updated: May 16 2021 at 20:13 UTC