inductive Set.IsExchange {α : Type u_1} : Set α → Set α → Prop

X.IsExchange Y means that Y is obtained from X by adding an element of Y \ X and then removing an element of X \ Y.

• insert_insert' {α : Type u_1} (X : Set α) (e f : α) (heX : e ∉ X) (hfX : f ∉ X) (hef : e ≠ f) : (insert e X).IsExchange (insert f X)

theorem Set.isExchange_insert_insert {α : Type u_1} {X : Set α} {e f : α} (heX : e ∉ X) (hfX : f ∉ X) (hef : e ≠ f) : (insert e X).IsExchange (insert f X)

theorem Set.IsExchange.symm {α : Type u_1} {X Y : Set α} (hXY : X.IsExchange Y) : Y.IsExchange X

theorem Set.isExchange_comm {α : Type u_1} {X Y : Set α} : X.IsExchange Y ↔ Y.IsExchange X

theorem Set.IsExchange.ne {α : Type u_1} {X Y : Set α} (hXY : X.IsExchange Y) : X ≠ Y

theorem Set.IsExchange.exists {α : Type u_1} {X Y : Set α} (hXY : X.IsExchange Y) : ∃ e ∈ X \ Y, ∃ f ∈ Y \ X, Y = insert f (X \ {e})

theorem Set.IsExchange.exists_sdiff_singleton_of_mem {α : Type u_1} {X Y : Set α} {e : α} (h : X.IsExchange Y) (heX : e ∈ X) (heY : e ∉ Y) : ∃ f ∈ Y, f ∉ X ∧ X = insert e (Y \ {f})

theorem Set.IsExchange.exists_insert_of_notMem {α : Type u_1} {X Y : Set α} {e : α} (h : X.IsExchange Y) (heX : e ∉ X) (heY : e ∈ Y) : ∃ f ∈ X, f ∉ Y ∧ X = insert f (Y \ {e})

theorem Set.isExchange_sdiff_insert {α : Type u_1} {X : Set α} {e f : α} (heX : e ∈ X) (hfX : f ∉ X) : X.IsExchange (insert f (X \ {e}))

theorem Set.isExchange_insert_sdiff {α : Type u_1} {X : Set α} {e f : α} (heX : e ∈ X) (hfX : f ∉ X) : X.IsExchange (insert f X \ {e})

theorem Set.isExchange_diff_singleton_diff_singleton {α : Type u_1} {X : Set α} {e f : α} (heX : e ∈ X) (hfX : f ∈ X) (hef : e ≠ f) : (X \ {e}).IsExchange (X \ {f})

theorem Set.IsExchange.diff_eq_singleton {α : Type u_1} {X Y : Set α} (h : X.IsExchange Y) : ∃ (e : α), X \ Y = {e}

theorem Set.IsExchange.union_union {α : Type u_1} {X Y P : Set α} (hXY : X.IsExchange Y) (hPX : Disjoint P X) (hPY : Disjoint P Y) : (X ∪ P).IsExchange (Y ∪ P)

theorem Set.IsExchange.insert_insert {α : Type u_1} {X Y : Set α} {e : α} (hXY : X.IsExchange Y) (heX : e ∉ X) (heY : e ∉ Y) : (insert e X).IsExchange (insert e Y)

theorem Set.IsExchange.sdiff_sdiff {α : Type u_1} {X Y P : Set α} (hXY : X.IsExchange Y) (hPX : P ⊆ X) (hPY : P ⊆ Y) : (X \ P).IsExchange (Y \ P)

theorem Set.IsExchange.nonempty_left {α : Type u_1} {X Y : Set α} (h : X.IsExchange Y) : X.Nonempty

theorem Set.IsExchange.nonempty_right {α : Type u_1} {X Y : Set α} (h : X.IsExchange Y) : Y.Nonempty

@[simp]

theorem Set.not_empty_isExchange {α : Type u_1} (X : Set α) : ¬∅.IsExchange X

@[simp]

theorem Set.not_isExchange_empty {α : Type u_1} (X : Set α) : ¬X.IsExchange ∅

theorem Set.IsExchange.sdiff_right {α : Type u_1} {X Y S : Set α} (h : X.IsExchange Y) (hXS : X ⊆ S) (hYS : Y ⊆ S) : (S \ X).IsExchange (S \ Y)

theorem Set.isExchange_sdiff_right_iff {α : Type u_1} {X Y S : Set α} (hXS : X ⊆ S) (hYS : Y ⊆ S) : (S \ X).IsExchange (S \ Y) ↔ X.IsExchange Y

theorem Set.isExchange_sdiff_right_comm {α : Type u_1} {X Y S : Set α} (hXS : X ⊆ S) (hYS : Y ⊆ S) : X.IsExchange (S \ Y) ↔ (S \ X).IsExchange Y

theorem Set.isExchange_insert_insert_iff {α : Type u_1} {X Y : Set α} {e : α} (heX : e ∉ X) (heY : e ∉ Y) : (insert e X).IsExchange (insert e Y) ↔ X.IsExchange Y

@[simp]

theorem Set.singleton_isExchange_iff {α : Type u_1} {X : Set α} {a : α} : {a}.IsExchange X ↔ ∃ (b : α), b ≠ a ∧ X = {b}

@[simp]

theorem Set.isExchange_singleton_iff {α : Type u_1} {X : Set α} {a : α} : X.IsExchange {a} ↔ ∃ (b : α), b ≠ a ∧ X = {b}

theorem Set.isExchange_singleton_singleton {α : Type u_1} {a b : α} : {a}.IsExchange {b} ↔ a ≠ b

@[simp]

theorem Set.isExchange_pair_iff_right {α : Type u_1} {a b c : α} : {a, b}.IsExchange {a, c} ↔ a ≠ b ∧ a ≠ c ∧ b ≠ c

@[simp]

theorem Set.isExchange_pair_iff_left {α : Type u_1} {a b c : α} : {a, c}.IsExchange {b, c} ↔ a ≠ b ∧ a ≠ c ∧ b ≠ c

theorem Set.isExchange_image_iff_of_injOn {α : Type u_1} {X Y : Set α} {β : Type u_2} {f : α → β} {S : Set α} (hS : InjOn f S) (hX : X ⊆ S) (hY : Y ⊆ S) : (f '' X).IsExchange (f '' Y) ↔ X.IsExchange Y

def Set.FinDiff {α : Type u_1} : Set α → Set α → Prop

X.FinDiff Y means that Y is obtained from X by inserting and then removing k elements, for some finite k.

Equations

• Set.FinDiff = Relation.ReflTransGen Set.IsExchange

theorem Set.FinDiff.symm {α : Type u_1} {X Y : Set α} (h : X.FinDiff Y) : Y.FinDiff X

theorem Set.finDiff_comm {α : Type u_1} {X Y : Set α} : X.FinDiff Y ↔ Y.FinDiff X

@[simp]

theorem Set.finDiff_refl {α : Type u_1} (X : Set α) : X.FinDiff X

theorem Set.FinDiff.encard_sdiff_comm {α : Type u_1} {X Y : Set α} (h : X.FinDiff Y) : (X \ Y).encard = (Y \ X).encard

theorem Set.FinDiff.eq_of_subset {α : Type u_1} {X Y : Set α} (h : X.FinDiff Y) (hXY : X ⊆ Y) : X = Y

theorem Set.FinDiff.sdiff_nonempty_of_ne {α : Type u_1} {X Y : Set α} (h : X.FinDiff Y) (hne : X ≠ Y) : (X \ Y).Nonempty

theorem Set.IsExchange.finDiff {α : Type u_1} {X Y : Set α} (h : X.IsExchange Y) : X.FinDiff Y

theorem Set.FinDiff.trans {α : Type u_1} {X Y Z : Set α} (hXY : X.FinDiff Y) (hYZ : Y.FinDiff Z) : X.FinDiff Z

theorem Set.FinDiff.trans_exchange {α : Type u_1} {X Y Z : Set α} (hXY : X.FinDiff Y) (hYZ : Y.IsExchange Z) : X.FinDiff Z

theorem Set.IsExchange.trans_finDiff {α : Type u_1} {X Y Z : Set α} (hXY : X.IsExchange Y) (hYZ : Y.FinDiff Z) : X.FinDiff Z

theorem Set.FinDiff.sdiff_finite {α : Type u_1} {X Y : Set α} (h : X.FinDiff Y) : (X \ Y).Finite

theorem Set.FinDiff.induction {α : Type u_1} {motive : (X Y : Set α) → X.FinDiff Y → Prop} (refl : ∀ (X : Set α), motive X X ⋯) (exchange : ∀ (X Y Z : Set α) (hXY : X.FinDiff Y) (hYZ : Y.IsExchange Z), Y ⊆ X ∪ Z → X ∩ Z ⊆ Y → motive X Y hXY → motive X Z ⋯) {X Y : Set α} (hXY : X.FinDiff Y) : motive X Y hXY

theorem Set.FinDiff.induction_head {α : Type u_1} {motive : (X Y : Set α) → X.FinDiff Y → Prop} (refl : ∀ (X : Set α), motive X X ⋯) (exchange : ∀ (X Y Z : Set α) (hXY : X.IsExchange Y) (hYZ : Y.FinDiff Z), Y ⊆ X ∪ Z → X ∩ Z ⊆ Y → motive Y Z hYZ → motive X Z ⋯) {X Y : Set α} (hXY : X.FinDiff Y) : motive X Y hXY

theorem Set.finDiff_insert_insert {α : Type u_1} {X : Set α} {e f : α} (heX : e ∉ X) (hfX : f ∉ X) : (insert e X).FinDiff (insert f X)

theorem Set.FinDiff.union_union_disjoint {α : Type u_1} {X Y P : Set α} (hXY : X.FinDiff Y) (hPX : Disjoint P X) (hPY : Disjoint P Y) : (X ∪ P).FinDiff (Y ∪ P)

theorem Set.FinDiff.sdiff_sdiff {α : Type u_1} {X Y P : Set α} (hXY : X.FinDiff Y) (hPX : P ⊆ X) (hPY : P ⊆ Y) : (X \ P).FinDiff (Y \ P)

theorem Set.finDiff_union_union_disjoint_iff {α : Type u_1} {X Y P : Set α} (hPX : Disjoint P X) (hPY : Disjoint P Y) : (X ∪ P).FinDiff (Y ∪ P) ↔ X.FinDiff Y

theorem Set.finDiff_iff {α : Type u_1} {X Y : Set α} : X.FinDiff Y ↔ (X \ Y).Finite ∧ (X \ Y).encard = (Y \ X).encard

theorem Set.finDiff_image_iff_of_injOn {α : Type u_1} {X Y S : Set α} {β : Type u_2} {f : α → β} (hS : InjOn f S) (hX : X ⊆ S) (hY : Y ⊆ S) : (f '' X).FinDiff (f '' Y) ↔ X.FinDiff Y

theorem Set.FinDiff.encard_eq_encard {α : Type u_1} {X Y : Set α} (h : X.FinDiff Y) : X.encard = Y.encard

theorem Set.FinDiff.sdiff_nonempty_of_nonempty {α : Type u_1} {X Y : Set α} (h : X.FinDiff Y) (hXY : (Y \ X).Nonempty) : (X \ Y).Nonempty

theorem Set.FinDiff.nonempty_of_nonempty {α : Type u_1} {X Y : Set α} (h : X.FinDiff Y) (hX : X.Nonempty) : Y.Nonempty

@[simp]

theorem Set.finDiff_singleton_singleton {α : Type u_1} (e f : α) : {e}.FinDiff {f}

theorem Set.FinDiff.union_union_right {α : Type u_1} {X Y P : Set α} (hXY : X.FinDiff Y) (hPX : Disjoint P X) (hPY : Disjoint P Y) : (X ∪ P).FinDiff (Y ∪ P)

theorem Set.FinDiff.sdiff_sdiff_right {α : Type u_1} {X Y P : Set α} (hXY : X.FinDiff Y) (hPX : P ⊆ X) (hPY : P ⊆ Y) : (X \ P).FinDiff (Y \ P)

theorem Set.FinDiff.finDiff_union_union_iff {α : Type u_1} {X Y P Q : Set α} (hPQ : P.FinDiff Q) (hPX : Disjoint P X) (hQY : Disjoint Q Y) : (X ∪ P).FinDiff (Y ∪ Q) ↔ X.FinDiff Y

theorem Set.FinDiff.finDiff_sdiff_sdiff_iff {α : Type u_1} {X Y P Q : Set α} (hPQ : P.FinDiff Q) (hPX : P ⊆ X) (hQY : Q ⊆ Y) : (X \ P).FinDiff (Y \ Q) ↔ X.FinDiff Y

theorem Set.finDiff_sdiff_sdiff_singleton_iff {α : Type u_1} {X Y : Set α} {e f : α} (heX : e ∈ X) (hfY : f ∈ Y) : (X \ {e}).FinDiff (Y \ {f}) ↔ X.FinDiff Y

theorem Set.FinDiff.finDiff_sdiff_sdiff_singleton {α : Type u_1} {X Y : Set α} {e f : α} (hXY : X.FinDiff Y) (heX : e ∈ X) (hfY : f ∈ Y) : (X \ {e}).FinDiff (Y \ {f})

theorem Set.finDiff_insert_insert_iff {α : Type u_1} {X Y : Set α} {e f : α} (heX : e ∉ X) (hfY : f ∉ Y) : (insert e X).FinDiff (insert f Y) ↔ X.FinDiff Y

theorem Set.FinDiff.union_union {α : Type u_1} {X Y P Q : Set α} (hXY : X.FinDiff Y) (hPQ : P.FinDiff Q) (hPX : Disjoint P X) (hQY : Disjoint Q Y) : (X ∪ P).FinDiff (Y ∪ Q)

theorem Set.FinDiff.insert_insert {α : Type u_1} {X Y : Set α} {e f : α} (hXY : X.FinDiff Y) (heX : e ∉ X) (hfY : f ∉ Y) : (insert e X).FinDiff (insert f Y)

theorem Set.FinDiff.exchange_right {α : Type u_1} {X Y : Set α} (hXY : X.FinDiff Y) {e f : α} (heY : e ∈ Y) (hfY : f ∉ Y) : X.FinDiff (insert f (Y \ {e}))

theorem Set.finDiff_iff_exchange {α : Type u_1} {X Y : Set α} {e f : α} (heY : e ∈ Y) (hfY : f ∉ Y) : X.FinDiff Y ↔ X.FinDiff (insert f (Y \ {e}))

theorem Set.FinDiff.sdiff_right {α : Type u_1} {X Y S : Set α} (h : X.FinDiff Y) (hXS : X ⊆ S) (hYS : Y ⊆ S) : (S \ X).FinDiff (S \ Y)

theorem Set.finDiff_sdiff_right_iff {α : Type u_1} {X Y S : Set α} (hXS : X ⊆ S) (hYS : Y ⊆ S) : (S \ X).FinDiff (S \ Y) ↔ X.FinDiff Y

theorem Set.finDiff_sdiff_right_comm {α : Type u_1} {X Y S : Set α} (hXS : X ⊆ S) (hYS : Y ⊆ S) : X.FinDiff (S \ Y) ↔ (S \ X).FinDiff Y

theorem Set.Finite.finDiff_iff_encard_eq {α : Type u_1} {X Y : Set α} (hX : X.Finite) : X.FinDiff Y ↔ X.encard = Y.encard