English
A predicate P on subsets satisfies the exchange property if for all X,Y with P X and P Y and all a in X\Y, there exists b in Y\X such that P(X\{a} ∪ {b}).
Русский
Предикат P на подмножества удовлетворяет свойству обмена: для любых X,Y с P X и P Y и любого a ∈ X\Y существует b ∈ Y\X such that P(X\{a} ∪ {b}).
LaTeX
$$$$ \forall \alpha \{P : Set \alpha \to \text{Prop}\} : \text{ExchangeProperty } P \iff \\forall X Y, P X \to P Y \to \forall a \in X \setminus Y, \exists b \in Y \setminus X, P \big(X \setminus \{a\} \cup \{b\}\big) $$$$
Lean4
/-- A predicate `P` on sets satisfies the **exchange property** if,
for all `X` and `Y` satisfying `P` and all `a ∈ X \ Y`, there exists `b ∈ Y \ X` so that
swapping `a` for `b` in `X` maintains `P`. -/
def ExchangeProperty {α : Type*} (P : Set α → Prop) : Prop :=
∀ X Y, P X → P Y → ∀ a ∈ X \ Y, ∃ b ∈ Y \ X, P (insert b (X \ { a }))
