English
Same content as mkRat_mem_ratLt, expressed under Archimedean context for the membership relation.
Русский
Та же концепция, что и mkRat_mem_ratLt, в контексте Архимедеан.
LaTeX
$$$\\mathrm{mkRat}(\\mathrm{num}, \\mathrm{den}) \\in \\mathrm{ratLt}(x) \\iff \\mathrm{num} \\cdot 1 < \\mathrm{den} \\cdot x.$$$
Lean4
theorem mkRat_mem_ratLt {num : ℤ} {den : ℕ} (hden : den ≠ 0) {x : M} : mkRat num den ∈ ratLt x ↔ num • 1 < den • x :=
by
rw [Set.mem_setOf]
obtain ⟨m, hm0, hnum, hden⟩ := Rat.mkRat_num_den hden (show mkRat num den = _ by rfl)
conv in num • 1 => rw [hnum, mul_comm, ← smul_smul, natCast_zsmul]
conv in den • x => rw [hden, mul_comm, ← smul_smul]
exact (smul_lt_smul_iff_of_pos_left (Nat.zero_lt_of_ne_zero hm0)).symm
