English
If a finite set s of functions has more than one element, then there exists a coordinate i such that the projection onto i has more than one value, and each fiber over a fixed value is a proper subset of s.
Русский
Если конечное множество функций s содержит более одного элемента, найдётся координата i, такая что проекция на i имеет более чем одно значение, и каждое ответвление по фиксированному значению i является строгим подмножеством s.
LaTeX
$$∃ i, 1 < #(image (· i) s) ∧ ∀ ai, s.filter (· i = ai) ⊂ s$$
Lean4
/-- If a Finset in a Pi type is nontrivial (has at least two elements), then
its projection to some factor is nontrivial, and the fibers of the projection
are proper subsets. -/
theorem exists_of_one_lt_card_pi {ι : Type*} {α : ι → Type*} [∀ i, DecidableEq (α i)] {s : Finset (∀ i, α i)}
(h : 1 < #s) : ∃ i, 1 < #(s.image (· i)) ∧ ∀ ai, s.filter (· i = ai) ⊂ s :=
by
simp_rw [one_lt_card_iff, Function.ne_iff] at h ⊢
obtain ⟨a1, a2, h1, h2, i, hne⟩ := h
refine ⟨i, ⟨_, _, mem_image_of_mem _ h1, mem_image_of_mem _ h2, hne⟩, fun ai => ?_⟩
rw [filter_ssubset]
obtain rfl | hne := eq_or_ne (a2 i) ai
exacts [⟨a1, h1, hne⟩, ⟨a2, h2, hne⟩]
