Lean4
/-- O(n). Approximate membership in the set, that is, whether some element in the
set is equivalent to this one in the preorder. This is useful primarily for stating
correctness properties; use `∈` for a version that actually uses the BST property
of the tree.
Amem 2 {1, 2, 3} = true
Amem 4 {1, 2, 3} = false
To see the difference with `Emem`, we need a preorder that is not a partial order.
For example, suppose we compare pairs of numbers using only their first coordinate. Then:
-- TODO: Verify below example
Emem (0, 1) {(0, 0), (1, 2)} = false
Amem (0, 1) {(0, 0), (1, 2)} = true
(0, 1) ∈ {(0, 0), (1, 2)} = true
The `∈` relation is equivalent to `Amem` as long as the `Ordnode` is well formed,
and should always be used instead of `Amem`. -/
def Amem [LE α] (x : α) : Ordnode α → Prop :=
Any fun y => x ≤ y ∧ y ≤ x
