mem_adjoin_iff — Mathlib

English

For subsets s and elements x, x ∈ adjoin_R s iff x ∈ Subring.closure(range(algebraMap R A) ∪ s).

Русский

Для подмножества s и элемента x: x ∈ adjoin_R s эквивалентно x ∈ Subring.closure(range(algebraMap R A) ∪ s).

LaTeX

$$$x \\in \\operatorname{adjoin}_R s \\iff x \\in \\operatorname{Subring.closure}(\\operatorname{range}(\\operatorname{algebraMap} R A) \\cup s)$$$

Lean4

theorem mem_adjoin_iff {s : Set A} {x : A} : x ∈ adjoin R s ↔ x ∈ Subring.closure (Set.range (algebraMap R A) ∪ s) := by
  rw [← Subalgebra.mem_toSubring, adjoin_eq_ring_closure]

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