mixed version of ssubset_trans

Stream: Is there code for X?

[Bernd Losert]

Is there a version of ssubset_trans but with (h' : b ⊆ c)?

[Eric Rodriguez]

docs#ssubset_trans

[Yaël Dillies]

docs#has_subset.subset.trans

[Eric Rodriguez]

docs#ssubset_of_ssubset_of_subset

[Yaël Dillies]

docs#has_subset.subset.trans_ssubset, docs#has_ssubset.ssubset.trans_subset

[Eric Rodriguez]

docs#has_ssubset.ssubset.trans_subset

[Eric Rodriguez]

semantic satiation :shock:

[Bernd Losert]

Thanks guys.

[Kyle Miller]

It looks like docs#ssubset_of_subset_of_ssubset and docs#ssubset_of_ssubset_of_subset should be marked @[trans], which would be useful for when calc is eventually fixed.

It's occurred to me that it would be useful (and seemingly possible) to have a fancier transitivity tactic that can look up trans lemmas given the LHS relations, so for example

transitivity _ ⊂ _ ⊆ _

where you can fill in those three underscores. (I suppose this is no different from calc _ ⊂ _ : _ ... ⊆ _ : _, just less noisy looking.)

[Kyle Miller]

Aside: would it be too weird if a ⊂ b ⊆ c parsed as a ⊂ b ∧ b ⊆ c? Languages like Mathematica and Python do this. Can Lean?

Would it be weird if "cute binders" supported this as well for chains of two relations, so for example ∀ (1 ≤ x < 10), 1 ≤ x^2 < 100? (Having seen the current implementation for cute binders, this might be asking too much.)

[Floris van Doorn]

∀ (1 ≤ x < 10), and for that matter, ∀ (1 ≤ x), always looks a little weird to me, like you're quantifying over all 1s.

[Kevin Buzzard]

Yeah I explicitly avoid that when blackboard lecturing. But for all eps>0 is fine; that's why we have it in mathlib even though it's gt

[Jake Levinson]

Kyle Miller said:

It looks like docs#ssubset_of_subset_of_ssubset and docs#ssubset_of_ssubset_of_subset should be marked @[trans], which would be useful for when calc is eventually fixed.

It's occurred to me that it would be useful (and seemingly possible) to have a fancier transitivity tactic that can look up trans lemmas given the LHS relations, so for example

transitivity _ ⊂ _ ⊆ _

where you can fill in those three underscores. (I suppose this is no different from calc _ ⊂ _ : _ ... ⊆ _ : _, just less noisy looking.)

Oh I really like this idea. I find this particular naming scheme relatively easy to remember, but this would be very readable.

@Bernd Losert Some of the lemma names given in this thread are analogous to le/lt lemmas such as lt_trans and lt_of_le_of_lt (analogous to ssubset_of_subset_of_ssubset).

[Kyle Miller]

Floris van Doorn said:

∀ (1 ≤ x), always looks a little weird to me, like you're quantifying over all 1s.

Yeah, that one fails the "abstraction test": ∀ (y ≤ x) shouldn't suddenly have completely different meaning.