subset_mulSpan — Mathlib

English

Every element of the finite set s lies in its span: s ⊆ mulSpan(s).

Русский

Каждый элемент множества s принадлежит его спану: s ⊆ mulSpan(s).

LaTeX

$$$s \subseteq mulSpan(s)$$$

Lean4

@[to_additive (attr := simp)]
theorem subset_mulSpan : s ⊆ mulSpan s := fun a ha ↦
  mem_mulSpan.2
    ⟨Pi.single a 1, fun b ↦ by obtain rfl | hab := eq_or_ne a b <;> simp [*], by
      simp [Pi.single, Function.update, pow_ite, ha]⟩

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