sup_le — Mathlib

English

If H holds and f ≤ h and g ≤ h, then the supremum f ⊔ g(H) is ≤ h.

Русский

Если условие совместимости H выполнено и f ≤ h, g ≤ h, тогда f ⊔ g(H) ≤ h.

LaTeX

$$$\text{If } H,\ f \le h,\ g \le h,\ \text{then } f \sup g H \le h$$$

Lean4

protected theorem sup_le {f g h : E →ₗ.[R] F} (H : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y)
    (fh : f ≤ h) (gh : g ≤ h) : f.sup g H ≤ h :=
  have Hf : f ≤ f.sup g H ⊓ h := le_inf (f.left_le_sup g H) fh
  have Hg : g ≤ f.sup g H ⊓ h := le_inf (f.right_le_sup g H) gh
  le_of_eqLocus_ge <| sup_le Hf.1 Hg.1

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