English
If e: X ≅ Y and IsLE X n, then IsLE Y n.
Русский
Если есть изоморфизм e: X ≅ Y и IsLE X n, то IsLE Y n.
LaTeX
$$$[t.IsLE X n] \\Rightarrow t.IsLE Y n$ for e: X \\cong Y.$$
Lean4
theorem ge_antitone : Antitone t.ge :=
by
let H := fun (a : ℕ) => ∀ (n : ℤ), t.ge (n + a) ≤ t.ge n
suffices ∀ (a : ℕ), H a by
intro n₀ n₁ h
obtain ⟨a, ha⟩ := Int.nonneg_def.1 h
obtain rfl : n₁ = n₀ + a := by cutsat
apply this
have H_zero : H 0 := fun n => by
simp only [Nat.cast_zero, add_zero]
rfl
have H_one : H 1 := fun n X hX =>
by
rw [← t.shift_ge n 1 (n + (1 : ℕ)) (by simp), ObjectProperty.prop_shift_iff] at hX
rw [← t.shift_ge n 0 n (add_zero n)]
exact t.ge_one_le _ hX
have H_add : ∀ (a b c : ℕ) (_ : a + b = c) (_ : H a) (_ : H b), H c :=
by
intro a b c h ha hb n
rw [← h, Nat.cast_add, ← add_assoc]
exact (hb (n + a)).trans (ha n)
intro a
induction a with
| zero => exact H_zero
| succ a ha => exact H_add a 1 _ rfl ha H_one
