Nat.le_lt_asymm

Stream: general

[Richard Copley]

Is the renaming of le_lt_antisymm to le_lt_asymm in std4#194 desirable? There is an asymmetry, but the lemma is about an antisymmetry.

[Richard Copley]

Also lt_antisymm to lt_asymm.

[Richard Copley]

But le_antisymm still has its old name.

[Scott Morrison]

@François G. Dorais?

[Yury G. Kudryashov]

I guess, antisymm is for r a b → s b a → a = b and asymm is for r a b → s b a → False.

[Yury G. Kudryashov]

E.g., docs#lt_asymm (came from Lean 3 core)

[François G. Dorais]

Yury is right. This change was requested by Mario.

[Scott Morrison]

Great, thanks. Do we have more to do to make Mathlib consistent with that naming scheme?

[Yury G. Kudryashov]

git grep 'antisymm.*¬' finds nothing

[Richard Copley]

Thanks.