mem_closure_iff — Mathlib

English

For a subfield s of K, an element x lies in closure(s) if and only if x can be expressed as a quotient of two elements from the closure of s in the Subring sense.

Русский

Элемент x принадлежит замыканию s тогда и только тогда, когда x может быть выражен как частное элементов из замыкания s внутри подполья.

LaTeX

$$$ x\\in \\mathrm{closure}(s) \\iff \\exists y,z\\in \\mathrm{closure}(s)\\, y/z = x $$$

Lean4

theorem mem_closure_iff {s : Set K} {x} : x ∈ closure s ↔ ∃ y ∈ Subring.closure s, ∃ z ∈ Subring.closure s, y / z = x :=
  by rw [← commClosure_eq_closure]; rfl

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