English
If j is a left inverse of i, then image-operator on Finset preserves Tendsto to atTop.
Русский
Если j — левобратная i, то образ-оператор Finset сохраняет предел к atTop.
LaTeX
$$$[\text{DecidableEq } \beta] \Rightarrow \operatorname{Tendsto}(\operatorname{Finset.image}(j), \operatorname{atTop}, \operatorname{atTop})$$$
Lean4
theorem eventually_pow_lt_factorial_sub (c d : ℕ) : ∀ᶠ n in atTop, c ^ n < (n - d)! :=
by
rw [eventually_atTop]
refine ⟨2 * (c ^ 2 + d + 1), ?_⟩
intro n hn
obtain ⟨d', rfl⟩ := Nat.exists_eq_add_of_le hn
obtain (rfl | c0) := c.eq_zero_or_pos
· simp [Nat.two_mul, ← Nat.add_assoc, Nat.add_right_comm _ 1, Nat.factorial_pos]
refine (Nat.le_mul_of_pos_right _ (Nat.pow_pos (n := d') c0)).trans_lt ?_
convert_to (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!
· rw [← pow_mul, ← pow_add]
congr 1
cutsat
· congr 1
cutsat
refine (lt_of_lt_of_le ?_ Nat.factorial_mul_pow_le_factorial).trans_le <| (factorial_le (Nat.le_succ _))
rw [← one_mul (_ ^ _ : ℕ)]
apply Nat.mul_lt_mul_of_le_of_lt
· exact Nat.one_le_of_lt (Nat.factorial_pos _)
· exact Nat.pow_lt_pow_left (Nat.lt_succ_self _) (Nat.succ_ne_zero _)
· exact (Nat.factorial_pos _)
