coe_single — Mathlib

English

If I and J are disjoint with univ ⊆ I ∪ J, then the supremum of the ranges of singles over I equals the infimum of the kernels of projections over J.

Русский

Если I и J дизъюнкты и выполнено univ ⊆ I ∪ J, то супремум образов одиночных отображений по I равен инфиминум веков проекций по J.

LaTeX

$$$⨆ i∈I,\\; \\mathrm{range}(\\text{single } i) = ⨅ i∈J, \\ker(\\mathrm{proj}_i).$$$

Lean4

@[simp]
theorem coe_single [DecidableEq ι] (i : ι) : ⇑(single R φ i : φ i →ₗ[R] (i : ι) → φ i) = Pi.single i :=
  rfl

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