toSubspace_isMono — Mathlib

English

Line toSubspace preserves monotonicity: l.toSubspace.IsMono C iff l.IsMono (λ x, C (fun (i,e) ↦ x i e)).

Русский

ПреобразованиеLine →Subspace сохраняет монотонность: l.toSubspace.IsMono C эквивалентно l.IsMono (λ x, C (λ (i,e), x i e)).

LaTeX

$$$\\forall {l : Line (\\eta \\to \\alpha) \\iota} {C : (Prod\\ ι\\ \\eta \\to \\alpha) \\to κ},\\ l.toSubspace.IsMono C \\iff l.IsMono (\\lambda x: ι \\to (\\eta \\to \\alpha) , C (\\lambda p, x p.1 p.2)).$$$

Lean4

@[simp]
theorem toSubspace_isMono {l : Line (η → α) ι} {C : (ι × η → α) → κ} :
    l.toSubspace.IsMono C ↔ l.IsMono fun x : ι → η → α ↦ C fun (i, e) ↦ x i e := by
  simp [Subspace.IsMono, IsMono, funext (toSubspace_apply _ _)]

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