English
If S Semiconjugates to T via φ, then coverMincard S F ((map φ φ)⁻¹'(V ○ V)) n ≤ coverMincard T (φ '' F) V n for all F, V, n.
Русский
Если S и T связаны через φ полиномом, то минимальная величина покрытия S на F через предобраз φ φ не превосходит минимальную величину покрытия T на φ(F) через V.
LaTeX
$$$\forall S,T,\forall F,\forall V,\forall n:\mathbb{N},\; \text{coverMincard } S\ F\ ((\text{map } φ φ)^{-1}'(V\circ V))\ n \le \text{coverMincard } T\ (φ''F)\ V\ n$$$
Lean4
theorem le_coverMincard_image (h : Semiconj φ S T) (F : Set X) {V : Set (Y × Y)} (V_symm : IsSymmetricRel V) (n : ℕ) :
coverMincard S F ((map φ φ) ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n :=
by
rcases eq_top_or_lt_top (coverMincard T (φ '' F) V n) with h' | h'
· exact h' ▸ le_top
obtain ⟨t, t_cover, t_card⟩ := (coverMincard_finite_iff T (φ '' F) V n).1 h'
obtain ⟨s, s_cover, s_card⟩ := t_cover.preimage h V_symm
rw [← t_card]
exact s_cover.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s_card)
