English
In a linearly ordered field, if f → C with C < 0 and g → atTop, then f·g → atBot.
Русский
В линейно упорядоченном поле, если f → C, где C < 0, а g → +∞, тогда f·g → −∞.
LaTeX
$$$\text{If } f\to C<0 \text{ and } g\to +\infty, \; f\cdot g \to -\infty.$$$
Lean4
instance (priority := 100) toContinuousInv₀ [ContinuousMul 𝕜] : ContinuousInv₀ 𝕜 :=
.of_nhds_one <|
tendsto_order.2 <| by
refine ⟨fun x hx => ?_, fun x hx => ?_⟩
· obtain ⟨x', h₀, hxx', h₁⟩ : ∃ x', 0 < x' ∧ x ≤ x' ∧ x' < 1 :=
⟨max x (1 / 2), one_half_pos.trans_le (le_max_right _ _), le_max_left _ _, max_lt hx one_half_lt_one⟩
filter_upwards [Ioo_mem_nhds one_pos ((one_lt_inv₀ h₀).2 h₁)] with y hy
exact hxx'.trans_lt <| lt_inv_of_lt_inv₀ hy.1 hy.2
· filter_upwards [Ioi_mem_nhds (inv_lt_one_of_one_lt₀ hx)] with y hy
exact inv_lt_of_inv_lt₀ (by positivity) hy
