left_le_sup — Mathlib

English

With the compatibility condition H, the first map f is contained in the supremum f ⊔ g(H).

Русский

При условии совместимости H первый отображатель f вложен в верхний предел f ⊔ g(H).

LaTeX

$$$f \le f \sup g\!\;H$$$

Lean4

protected theorem left_le_sup (f g : E →ₗ.[R] F) (h : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) :
    f ≤ f.sup g h := by
  refine ⟨le_sup_left, fun z₁ z₂ hz => ?_⟩
  rw [← add_zero (f _), ← g.map_zero]
  refine (sup_apply h _ _ _ ?_).symm
  simpa

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