of_subset_of_superset — Mathlib

English

If s is GLB a and p is GLB a, and s ⊆ t ⊆ p, then t is GLB a.

Русский

Если s и p имеют GLB в точке a, и s ⊆ t ⊆ p, то t имеет GLB a.

LaTeX

$${s t p : Set α} (hs : IsGLB s a) (hp : IsGLB p a) (hst : s ⊆ t) (htp : t ⊆ p) : IsGLB t a$$

Lean4

/-- If `a` is a greatest lower bound for sets `s` and `p`, then it is a greater lower bound for any
set `t`, `s ⊆ t ⊆ p`. -/
theorem of_subset_of_superset {s t p : Set α} (hs : IsGLB s a) (hp : IsGLB p a) (hst : s ⊆ t) (htp : t ⊆ p) :
    IsGLB t a :=
  hs.dual.of_subset_of_superset hp hst htp

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