English
Let S and T be endomorphisms on X and Y respectively, and φ: X → Y a semiconjugacy from S to T. For any subset F ⊆ X, any relation V ⊆ Y × Y, and any natural number n, the minimal cover size after transporting F along φ is bounded above by the corresponding minimal cover size of F with the preimage of V under the product map φ × φ.
Русский
Пусть S и T — отображения на X и Y, соответственно, и φ: X → Y является семиконъюгатом S к T. Для любого подмножества F ⊆ X, отношения V ⊆ Y × Y и натурального n, минимальное число множества, покрывающее φ(F) по V, не превосходит аналогичное число для F по ((φ × φ)^{-1}(V)).
LaTeX
$$$\\operatorname{coverMincard}(T, \\phi(F), V, n) \\le \\operatorname{coverMincard}(S, F, (\\phi \\times \\phi)^{-1}(V), n)$$$
Lean4
theorem coverMincard_image_le (h : Semiconj φ S T) (F : Set X) (V : Set (Y × Y)) (n : ℕ) :
coverMincard T (φ '' F) V n ≤ coverMincard S F ((map φ φ) ⁻¹' V) n := by
classical
rcases eq_top_or_lt_top (coverMincard S F ((map φ φ) ⁻¹' V) n) with h' | h'
· exact h' ▸ le_top
obtain ⟨s, s_cover, s_card⟩ := (coverMincard_finite_iff S F ((map φ φ) ⁻¹' V) n).1 h'
rw [← s_card]
have := s_cover.image h
rw [← s.coe_image] at this
exact this.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s.card_image_le)
