coe_sInf' — Mathlib

English

The α-value of the infimum of S equals the infimum over N ∈ S of N’s α-values.

Русский

Значение в α наименьшей границы множества S равно наименьшей границе по α элементов S.

LaTeX

$$$\left(\uparrow(\mathrm{sInf} S) : α\right) = \bigwedge_{N \in S} (N : α)$$$

Lean4

theorem coe_sInf' (S : Set L) : (↑(sInf S) : α) = ⨅ N ∈ S, (N : α) := by rw [coe_sInf, ← Set.image, sInf_image]

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