English
If x is not in the domain of f, then f.eval x is different from every f.y with y in f.val.domain.
Русский
Если x не принадлежит области определения f, то f.eval x не равно ни одному значению f.val y при y из области определения f.
LaTeX
$$$\\forall y\\in f.val.domain:\\; f.eval(x) \\neq f.val(y)$, если $x\\notin f.val.domain$.$$
Lean4
/-- If `x` isn't in `f`'s domain, `f.eval x` produces a brand new value not in `f`'s range. -/
theorem eval_ne [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ f.val.domain) (y : f.val.domain) :
f.eval x ≠ f.val y :=
by
have hxy0 : mk (x - y.val) ≠ ⊤ := by
contrapose! hx with hxy
rw [mk_eq_top_iff, sub_eq_zero] at hxy
rw [hxy]
exact y.prop
have hxy : x - y.val ∈ closedBall K (mk (x - y.val)) := by simp
rw [← seed.ball_sup_stratum_eq (mk (x - y.val)), Submodule.mem_sup] at hxy
obtain ⟨u, hu, v, hv, huv⟩ := hxy
have huv' : x - y.val - v = u := by simp [← huv]
rw [mem_ball_iff K hxy0] at hu
have hyv : y.val + v ∈ f.val.domain := Submodule.add_mem _ (by simp) (f.mem_domain hv)
by_contra! h
obtain h := f.archimedeanClassMk_le_of_eval_eq h ⟨y.val + v, hyv⟩
contrapose! h
simpa [← sub_sub, huv'] using hu
