English
embedRealFun maps 0 to 0.
Русский
embedRealFun(0) = 0.
LaTeX
$$$\operatorname{embedRealFun}(0) = 0$$$
Lean4
theorem embedRealFun_zero : embedRealFun (0 : M) = 0 :=
by
apply le_antisymm
· apply csSup_le (ratLt'_nonempty 0)
intro x
unfold ratLt' ratLt
suffices ∀ (y : ℚ), y.num • (1 : M) < 0 → y = x → x ≤ 0 by simpa using this
intro y hy hyx
rw [← hyx, Rat.cast_nonpos, ← Rat.num_nonpos]
exact (neg_of_smul_neg_right hy zero_le_one).le
· rw [le_csSup_iff (ratLt'_bddAbove (0 : M)) (ratLt'_nonempty 0)]
intro x
rw [mem_upperBounds]
suffices (∀ (y : ℚ), y.num • (1 : M) < 0 → y ≤ x) → 0 ≤ x by simpa using this
intro h
have h' (y : ℚ) (hy : y < 0) : y ≤ x := by
exact h _ <| (smul_neg_iff_of_neg_left (by simpa using hy)).mpr zero_lt_one
contrapose! h'
obtain ⟨y, hxy, hy⟩ := exists_rat_btwn h'
exact ⟨y, by simpa using hy, hxy⟩
