## 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 11 2021 at 16:22 UTC