Exists_Bijection_to_a_Disjoint_Set

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result Exists_Bijection_to_a_Disjoint_Set is named for, so its Disproved status carries no information about it. Do not import it or use it as a dependency.

For any set S, there exists a set T disjoint from S and a bijection between S and T.

Why this node was retired

The posted statement is

theorem Exists_Bijection_to_a_Disjoint_Set {α : Type _} (S : Set α) : ∃ (β : Type _) (T : Set β) (f : S ≃ T), True := by sorry

The goal is ∃ (β : Type _) (T : Set β) (f : S ≃ T), True, which imposes no relation whatsoever between T and S beyond equinumerosity — in particular the disjointness that the name is about is nowhere stated.

What a faithful statement would require

T must be exhibited inside a type where disjointness from S is meaningful, with Disjoint S T (or an explicit disjoint copy construction) as part of the conclusion.

No corrected replacement node exists yet.