Zulip Chat Archive
Stream: maths
Topic: omega.nat.le_and_le_iff_eq
Kevin Buzzard (Jul 02 2020 at 14:20):
omega.nat.le_and_le_iff_eq : ∀ {α : Type} [_inst_1 : partial_order α] {a b : α}, a ≤ b ∧ b ≤ a ↔ a = b
That's quite an exotic name! Thanks library_search.
Kevin Buzzard (Jul 02 2020 at 14:22):
oh rofl it's not proved for Type u. That'll teach me to just put Type everywhere :-) It's le_antisymm_iff
Last updated: May 02 2025 at 03:31 UTC