span_mono

Mathlib.RingTheory.TwoSidedIdeal.Operations

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.span_mono

English

The same monotonicity of span with respect to subset relation for sets: if s ⊆ t then span s ≤ span t.

Русский

То же свойство монотонности span в отношении вложенности: если s ⊆ t, то span s ≤ span t.

LaTeX

$$s ⊆ t → span s ≤ span t$$

Lean4

theorem span_mono {s t : Set R} (h : s ⊆ t) : span s ≤ span t :=
  by
  intro x hx
  rw [mem_span_iff] at hx ⊢
  exact fun I hI => hx I <| h.trans hI

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru