instInfSet — Mathlib

English

Infimum structure on Sublocale is defined by taking the infimum in the ambient lattice of X of the images of elements of a set x ⊆ S, together with a membership proof.

Русский

Для S подлокаль задаётся InfSet: инфимум множества элементов x ⊆ S берётся как инфимум в X от образов элементов x, вместе с доказательством принадлежности.

LaTeX

$$$\text{InfSet}_S(x) = \langle \operatorname{sInf}(\operatorname{Subtype.val}'' x), \; \text{proof of membership} \rangle$$$

Lean4

instance instInfSet : InfSet S where
  sInf x := ⟨sInf (Subtype.val '' x), S.sInf_mem' _ (by simp_rw [image_subset_iff, subset_def]; simp)⟩

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