Finite set is union of smaller set and singleton

Stream: new members

[Sebastian Monnet]

If $S$ is a finite set of size $n$, then I want to state the fact that $S = T \cup \{x\}$ for some $x$, and $T$ has size $n-1$. I'm trying to state this as

example (X : Type*) (S : set X) (h_finite : S.finite) :
∃ (T : set X), ∃ (x : X), ∃ (h_T_finite : T.finite), (h_T_finite.to_finset.card = h_finite.to_finset.card - 1) ∧ (S = (T ⋃ ({x} : set X))) :=
sorry

but I get the error invalid definition, '|' or ':=' expected, along with a bunch of red lines under the (T ⋃ ({x} : set X)). Can anyone help?

[Yaël Dillies]

Are you sure you don't want to use docs#finset? Sounds a bit easier than what you're trying.

[Yaël Dillies]

You used the wrong symbol. It's not ⋃but ∪.

example (X : Type*) (S : set X) (h_finite : S.finite) :
∃ (T : set X), ∃ (x : X), ∃ (h_T_finite : T.finite), (h_T_finite.to_finset.card = h_finite.to_finset.card - 1) ∧ (S = (T ∪ ({x} : set X))) :=

[Patrick Massot]

This almost surely a #xy issue.

[Yakov Pechersky]

In any case, you can construct T from "erase x S" where you get x from deconstructing "S.nonempty". Which you do have, right? Because your statement is false for n = 0. I also agree with Patrick here.

[Sebastian Monnet]

Thank you @Yaël Dillies. Yes, it probably will turn out to be an XY issue. I asked for help with Y because I'd like to attempt X myself before someone tells me the "right" way to do it