inter_Iic_of_mem — Mathlib

English

If a is the greatest lower bound of s and a₂ is the greatest lower bound of t in a SemilatticeInf, then a₁ ⊓ a₂ is the greatest lower bound of s ∪ t.

Русский

Если a₁ — наибольшая нижняя граница s, а a₂ — наибольшая нижняя граница t в полулинейном инф-обратном порядке, то a₁ ⊓ a₂ — наибольшая нижняя граница s ∪ t.

LaTeX

$$$[SemilatticeInf γ] \; {a₁ a₂ : γ} {s t : Set γ} (hs : IsGLB s a₁) (ht : IsGLB t a₂) : IsGLB (s \cup t) (a₁ \inf a₂)$$$

Lean4

theorem inter_Iic_of_mem [LinearOrder γ] {s : Set γ} {a b : γ} (ha : IsGLB s a) (hb : b ∈ s) : IsGLB (s ∩ Iic b) a :=
  ha.dual.inter_Ici_of_mem hb

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