inf_mem_infClosure — Mathlib

English

If a and b belong to s, then their infimum a ∧ b belongs to infClosure(s).

Русский

Если a и b принадлежат s, то их наименьшее верхнее? нижнее? — инфимум a ∧ b принадлежит infClosure(s).

LaTeX

$$$a \in s \to b \in s \to a \wedge b \in \infClosure s$$$

Lean4

theorem inf_mem_infClosure (ha : a ∈ s) (hb : b ∈ s) : a ⊓ b ∈ infClosure s :=
  infClosed_infClosure (subset_infClosure ha) (subset_infClosure hb)

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