English
If F maps to itself under T and U is symmetric, then coverMincard with U○U at index m·n is bounded by the m-cover raised to the n-th power: coverMincard T F (U○U) (m·n) ≤ (coverMincard T F U m)^{n}.
Русский
Если F отображается в FT по T и U симметрично, то покрытие с U○U на m·n не больше (coverMincard T F U m)^n.
LaTeX
$$$coverMincard(T,F,(U\circ U),(m\cdot n))\le (coverMincard(T,F,U,m))^{n}$$$
Lean4
theorem coverMincard_mul_le_pow {T : X → X} {F : Set X} (F_inv : MapsTo T F F) {U : Set (X × X)}
(U_symm : IsSymmetricRel U) (m n : ℕ) : coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n :=
by
rcases F.eq_empty_or_nonempty with rfl | F_nonempty
· rw [coverMincard_empty]; exact zero_le _
obtain rfl | hn := eq_or_ne n 0
· rw [mul_zero, coverMincard_zero T F_nonempty (U ○ U), pow_zero]
rcases eq_top_or_lt_top (coverMincard T F U m) with h | h
· simp [*]
· obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U m).1 h
obtain ⟨t, t_cover, t_sn⟩ := s_cover.iterate_le_pow F_inv U_symm n
rw [← s_coverMincard]
exact t_cover.coverMincard_le_card.trans (WithTop.coe_le_coe.2 t_sn)
