subfield_eq_of_closed — Mathlib

English

If a subfield K of ℝ is closed as a subset of ℝ, then K is all of ℝ.

Русский

Если подполе K ⊆ ℝ замкнуто как множество в ℝ, то K = ℝ.

LaTeX

$$$K = \mathbb{R}$, если $K$ — замкнутое подполе ℝ$$

Lean4

theorem subfield_eq_of_closed {K : Subfield ℝ} (hc : IsClosed (K : Set ℝ)) : K = ⊤ :=
  by
  rw [SetLike.ext'_iff, Subfield.coe_top, ← hc.closure_eq]
  refine Rat.denseRange_cast.mono ?_ |>.closure_eq
  rintro - ⟨_, rfl⟩
  exact SubfieldClass.ratCast_mem K _

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