finsupport_subset_fintsupport — Mathlib

English

For every x0, finsupport x0 is contained in finsupport x0 by the subset relation.

Русский

Для любого x0 выполняется включение finsupport x0 в finsupport x0 (тривиально).

LaTeX

$$$ρ.finsupport x_0 ⊆ ρ.fintsupport x_0$$$

Lean4

theorem finsupport_subset_fintsupport : ρ.finsupport x₀ ⊆ ρ.fintsupport x₀ := fun i hi ↦
  by
  rw [ρ.mem_fintsupport_iff]
  apply subset_closure
  exact (ρ.mem_finsupport x₀).mp hi

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