span_le — Mathlib

English

Let R be a ring and I a two-sided ideal. For any subset s of R, the span of s is contained in I if and only if s is contained in I.

Русский

Пусть R — кольцо и I — двусторонний идеал. Для произвольного подмножества s ⊆ R выполняется: span(s) ⊆ I тогда и только тогда, когда s ⊆ I.

LaTeX

$$$\\displaystyle \\operatorname{span}(s) \\subseteq I \\iff s \\subseteq I$$$

Lean4

theorem span_le {s : Set R} {I : TwoSidedIdeal R} : span s ≤ I ↔ s ⊆ I :=
  by
  rw [TwoSidedIdeal.ringCon_le_iff, RingCon.gi _ |>.gc]
  exact ⟨fun h x hx ↦ by aesop, fun h x y hxy ↦ (rel_iff I x y).mpr (h hxy)⟩

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