English
If t is a nontrivial finite set, then a clique of G.map f on t corresponds to a finite clique in G via some finite s with s.map f = t.
Русский
Если t — не тривиальная конечная Superset, то клика графа G.map f на t соответствует конечной клике графа G на некотором Finset s с использованием отображения f (то есть s.map f = t).
LaTeX
$$$t\\text{ Nontrivial} \\Rightarrow\\ ((G.map\\ f).IsClique\\ t \\iff \\exists s:\\ Finset\\ α,\\ G.IsClique\\ s \\land s.map\\ f = t)$$$
Lean4
theorem isClique_map_finset_iff_of_nontrivial (ht : t.Nontrivial) :
(G.map f).IsClique t ↔ ∃ (s : Finset α), G.IsClique s ∧ s.map f = t :=
by
constructor
· rw [isClique_map_iff_of_nontrivial (by simpa)]
rintro ⟨s, hs, hst⟩
obtain ⟨s, rfl⟩ :=
Set.Finite.exists_finset_coe <| (show s.Finite from Set.Finite.of_finite_image (by simp [hst]) f.injective.injOn)
exact ⟨s, hs, Finset.coe_inj.1 (by simpa)⟩
rintro ⟨s, hs, rfl⟩
simpa using hs.map (f := f)
