subset_lieSpan — Mathlib

English

Let R, L, M be as above and s be any subset of M. Then every element of s lies in the Lie-span of s, i.e. s is contained in lieSpan(R,L,s).

Русский

Пусть R, L, M удовлетворяют условиям задачи, и s — произвольный подмножество M. Тогда каждый элемент s принадлежит lieSpan(R,L,s); то есть s ⊆ lieSpan(R,L,s).

LaTeX

$$$s \\subseteq \\operatorname{lieSpan}_{R,L}(s)$$$

Lean4

theorem subset_lieSpan : s ⊆ lieSpan R L s := by
  intro m hm
  rw [SetLike.mem_coe, mem_lieSpan]
  intro N hN
  exact hN hm

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