English
The cliqueSet of a mapped graph equals the image of the cliqueSet under the mapping, for n ≠ 1.
Русский
cliqueSet графа, полученного после отображения, равен образу cliqueSet исходного графа под отображением; верно при $n\neq1$.
LaTeX
$$For $n\neq 1$, $(G.map\ f).cliqueSet(n) = \operatorname{image}(\operatorname{Finset.map}(f))(G.cliqueSet(n))$.$$
Lean4
@[simp]
theorem cliqueSet_map (hn : n ≠ 1) (G : SimpleGraph α) (f : α ↪ β) : (G.map f).cliqueSet n = map f '' G.cliqueSet n :=
by
ext s
constructor
· rintro ⟨hs, rfl⟩
have hs' : (s.preimage f f.injective.injOn).map f = s := by
classical
rw [map_eq_image, image_preimage, filter_true_of_mem]
rintro a ha
obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
obtain ⟨c, _, _, hc, _⟩ := hs ha hb hba.symm
exact ⟨c, hc⟩
refine ⟨s.preimage f f.injective.injOn, ⟨?_, by rw [← card_map f, hs']⟩, hs'⟩
rw [coe_preimage]
exact fun a ha b hb hab => map_adj_apply.1 (hs ha hb <| f.injective.ne hab)
· rintro ⟨s, hs, rfl⟩
exact hs.map
