English
If F maps to itself under T and U is symmetric, then for m>0 and any n we have coverMincard T F (U○U) n ≤ (coverMincard T F U m)^{(n/m)+1}.
Русский
Если F отображается в себя по T и U симметрично, то для любых n и m>0 выполняется: coverMincard T F (U○U) n ≤ (coverMincard T F U m)^{(n/m)+1}.
LaTeX
$$$\text{If }F\ maps\ to\ itself\ under\ T\text{ and }U\text{ symmetric:} \ coverMincard(T,F,(U\circ U),n) \le (coverMincard(T,F,U,m))^{(n/m)+1}$$$
Lean4
theorem coverMincard_le_pow {T : X → X} {F : Set X} (F_inv : MapsTo T F F) {U : Set (X × X)} (U_symm : IsSymmetricRel U)
{m : ℕ} (m_pos : 0 < m) (n : ℕ) : coverMincard T F (U ○ U) n ≤ coverMincard T F U m ^ (n / m + 1) :=
(coverMincard_monotone_time T F (U ○ U) (Nat.lt_mul_div_succ n m_pos).le).trans
(coverMincard_mul_le_pow F_inv U_symm m (n / m + 1))
