Question about formalization in set theory.

Stream: maths

[Brisal]

Hello! I have recently been practicing formalization in Lean 4, specifically in graph theory and set theory. I would like to formalize this problem (currently without the proof part).

Let A_1, ..., A_n be n distinct subsets of the n-set N = {1, ..., n}.
Show that there exists an element x in N such that all the sets A_i without x (for i from 1 to n) are distinct.

I'm not sure whether It is right or not:

example {n : ℕ}
    (A : Finset.Icc 1 n → Finset (Finset.Icc 1 n))
    (h_distinct : Function.Injective A) :
    ∃ x : Finset.Icc 1 n, Function.Injective (fun i => (A i).erase x) := by
    sorry

Previously I was using Finset (Fin n), but I noticed that in the problem both the indices and elements start from 1, so I replaced it with Finset (Finset.Icc 1 n). Is this okay?

[Kenny Lau]

a nitpick, but this doesn't feel like set theory

[Kenny Lau]

do you have to follow the problem to the t?

[Brisal]

Kenny Lau said:

a nitpick, but this doesn't feel like set theory

Yes, this problem is from the graph theory section in the textbook.

[Kenny Lau]

because the first observation I would make is that 1. the indexing doesn't matter, and 2. the underlying n-set also doesn't matter

[Brisal]

Kenny Lau said:

because the first observation I would make is that 1. the indexing doesn't matter, and 2. the underlying n-set also doesn't matter

like this?

example {n : ℕ} (hn : 1 ≤ n)
    (A : Fin n → Finset (Fin n))
    (h_distinct : Function.Injective A) :
    ∃ x : Fin n, Function.Injective (fun i => (A i).erase x) := by
  sorry

[Kenny Lau]

yes

[Brisal]

Kenny Lau said:

yes

Thank you for your suggestion. Does this formalization have any other issues, or do you have any better recommendations? I would like to learn about it.

[Kenny Lau]

nope, that looks good

[Brisal]

Kenny Lau said:

nope, that looks good

Thank you for your reply