bot_le v zero_le

Stream: general

[Kevin Buzzard]

import tactic

#check @bot_le -- ∀ {a : α}, ⊥ ≤ a
#check @zero_le -- ∀ (a : α), 0 ≤ a

Why the difference in binders? I omitted the typeclasses; for bot_le it's [has_le α] [order_bot α] and for zero_le it's [canonically_ordered_add_monoid α]

[Eric Wieser]

I think the style guides are ambiguous with how to deal with ≤

[Eric Wieser]

On the one hand, the argument could be explicit because ≤ is like =

[Eric Wieser]

On the other, A ≤ B is often defeq to x ∈ A → x ∈ B, where x, A, and maybe B would then usually be made explicit

[Yaël Dillies]

I would make it explicit. ≤ is rarely defeq to x ∈ A → x ∈ B, especially when dealing with a 0 in the order and even ⊆ lemmas often have (over)explicit arguments.

[Kevin Buzzard]

In my experience <= is often defeq to the implication because I'm usually dealing with submodules, ideals, subspaces etc rather than these order types

[Damiano Testa]

I often found that I wished an argument was explicit, rather than being annoyed by it being not implicit. Hence, my preference would be to make them explicit!

[Adam Topaz]

+1 from me for making it explicit.

[Adam Topaz]

Same goes for docs#inf_le_left and its friends

[Yaël Dillies]

For the record, I just wrote @inf_comm _ _ a :grinning: