mem_span_iff — Mathlib

English

If s ⊆ t for sets of a ring, then span(s) ≤ span(t).

Русский

Если s ⊆ t для множеств кольца, то span(s) ≤ span(t).

LaTeX

$$s ⊆ t → span(s) ≤ span(t)$$

Lean4

theorem mem_span_iff {s : Set R} {x} : x ∈ span s ↔ ∀ (I : TwoSidedIdeal R), s ⊆ I → x ∈ I :=
  by
  refine ⟨?_, fun h => h _ subset_span⟩
  delta span
  rw [RingCon.ringConGen_eq]
  intro h I hI
  refine sInf_le (α := RingCon R) ?_ h
  intro x y hxy
  specialize hI hxy
  rwa [SetLike.mem_coe, ← rel_iff] at hI

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