law le_antisymm_eq

bend-mathlib@0.8.1.0 · order.bend:41

import Base

41# Antisymmetry gives equality.
42law le_antisymm_eq:
43  for ~A: Data
44  for ~le: A -> A -> Bool
45  for ~le_antisymm: @x: A -> @y: A -> {le(x, y) == True{} : Bool} -> {le(y, x) == True{} : Bool} -> {x == y : A}
46  for +a: A
47  for +b: A
48  for ab: {le(a, b) == True{} : Bool}
49  for ba: {le(b, a) == True{} : Bool}
50  {a == b : A}