lowerBounds_mono_of_isCoinitialFor

English

If s is IsCoinitialFor s t, then lowerBounds(t) ⊆ lowerBounds(s).

Русский

Если s является IsCoinitialFor относительно s и t, то множества нижних границ удовлетворяют включению: lowerBounds(t) ⊆ lowerBounds(s).

LaTeX

$$$ IsCoinitialFor(s,t) \Rightarrow lowerBounds(t) \subseteq lowerBounds(s) $$$

Lean4

@[gcongr]
theorem lowerBounds_mono_of_isCoinitialFor (hst : IsCoinitialFor s t) : lowerBounds t ⊆ lowerBounds s :=
  fun _a ha _b hb ↦
  let ⟨_c, hc, hcb⟩ := hst hb;
  hcb.trans' (ha hc)

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