coe_infs — Mathlib

English

Under the natural embedding into sets, the set of infima s ⊼ t corresponds to the set of pairwise infima a ⊓ b with a ∈ s and b ∈ t.

Русский

При естественном отображении в множества, множество инфимумов s ⊼ t соответствует множеству попарных инфимумов a ⊓ b с a ∈ s и b ∈ t.

LaTeX

$$$ (\uparrow(s ⊼ t) : Set \alpha) = \uparrow s \sqcap \uparrow t $$$

Lean4

@[simp, norm_cast]
theorem coe_infs : (↑(s ⊼ t) : Set α) = ↑s ⊼ ↑t :=
  coe_image₂ _ _ _

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