comap_cast_atBot — Mathlib

English

Similarly, comapping the bottom filter along the rational embedding into R yields the bottom filter.

Русский

Аналогично, обратное отображение нижнего фильтра через вложение рациональных чисел в R даёт нижний фильтр.

LaTeX

$$$\operatorname{comap}((\uparrow) : \mathbb{Q} \to R) \ \mathrm{atBot} = \mathrm{atBot}$$$

Lean4

@[simp]
theorem comap_cast_atBot [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] :
    comap ((↑) : ℚ → R) atBot = atBot :=
  comap_embedding_atBot (fun _ _ => Rat.cast_le) fun r =>
    let ⟨n, hn⟩ := exists_nat_ge (-r)
    ⟨-n, by simpa [neg_le]⟩

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