range_natAdd_castLEEmb — Mathlib

English

If hmn : n ≤ m, the range of natAdd_castLEEmb hmn equals {i ∈ Fin(m) | m − n ≤ i.1}.

Русский

Пусть hmn: n ≤ m. Тогда образ natAdd_castLEEmb hmn равен { i ∈ Fin(m) | m − n ≤ i.1 }.

LaTeX

$$$\mathrm{range}(\mathrm{natAdd\_castLEEmb}\ hmn) = \{ i : \mathrm{Fin}(m) \mid m-n \le i.1 \}$$$

Lean4

theorem range_natAdd_castLEEmb {n m : ℕ} (hmn : n ≤ m) : Set.range (natAdd_castLEEmb hmn) = {i | m - n ≤ i.1} :=
  by
  simp only [natAdd_castLEEmb, Nat.sub_le_iff_le_add]
  ext y
  exact
    ⟨fun ⟨x, hx⟩ ↦ by simp [← hx]; cutsat, fun xin ↦
      ⟨subNat (m - n) (y.cast (Nat.add_sub_of_le hmn).symm) (Nat.sub_le_of_le_add xin), by simp⟩⟩

Похожие утверждения