English
For an injective map f, and t Nontrivial, (G.map f).IsClique t iff there exists s with G.IsClique s and f'' s = t.
Русский
Для внедренного отображения f и множества t, не тривиального, (G.map f).IsClique t эквивалентно существованию множества s, такого что G.IsClique s и f'' s = t.
LaTeX
$$$ {f : \alpha \hookrightarrow \beta} {t : Set \beta} (ht : t.Nontrivial) : (G.map f).IsClique t \iff \exists (s : Set \alpha), G.IsClique s \land f '' s = t $$$
Lean4
theorem isClique_map_iff_of_nontrivial {f : α ↪ β} {t : Set β} (ht : t.Nontrivial) :
(G.map f).IsClique t ↔ ∃ (s : Set α), G.IsClique s ∧ f '' s = t :=
by
refine ⟨fun h ↦ ⟨f ⁻¹' t, ?_, ?_⟩, by rintro ⟨x, hs, rfl⟩; exact hs.map⟩
· rintro x (hx : f x ∈ t) y (hy : f y ∈ t) hne
obtain ⟨u, v, huv, hux, hvy⟩ := h hx hy (by simpa)
rw [EmbeddingLike.apply_eq_iff_eq] at hux hvy
rwa [← hux, ← hvy]
rw [Set.image_preimage_eq_iff]
intro x hxt
obtain ⟨y, hyt, hyne⟩ := ht.exists_ne x
obtain ⟨u, v, -, rfl, rfl⟩ := h hyt hxt hyne
exact Set.mem_range_self _
