span_coe — Mathlib

English

The infimum (greatest lower bound) of two subspaces exists in the lattice of subspaces.

Русский

Существует наименьшее сверху подпространство (наибольшее нижнее ограничение) для двух подпространств.

LaTeX

$$$\inf\{A,B\} \text{ exists in } \mathrm{Subspace}(K,V)$$$

Lean4

/-- The span of a subspace is the subspace. -/
@[simp]
theorem span_coe (W : Subspace K V) : span ↑W = W :=
  GaloisInsertion.l_u_eq gi W

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