right_le_sup — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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