inf_mem_infs — Mathlib

English

Let S and T be subsets of a semilattice with infimum. If a ∈ S and b ∈ T, then a ∧ b ∈ S ⊼ T, where S ⊼ T denotes { x ∧ y : x ∈ S, y ∈ T }.

Русский

Пусть S и T — подмножества полупорядоченного множества с операцией наименьшего нижнего ограничения. Тогда для любых a ∈ S и b ∈ T верно a ∧ b ∈ S ⊼ T, где S ⊼ T обозначает { x ∧ y | x ∈ S, y ∈ T }.

LaTeX

$$$ a \in s \rightarrow b \in t \rightarrow a \wedge b \in \{ x \wedge y \mid x \in s, y \in t \}$$$

Lean4

theorem inf_mem_infs : a ∈ s → b ∈ t → a ⊓ b ∈ s ⊼ t :=
  mem_image2_of_mem

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