coe_inf' — Mathlib

English

The coercion commutes with inf' on Finset: (s.inf' H f) coerces to (s.inf' H (λ i, f(i) coerced)).

Русский

Коэрцирование сохраняет инф'_по-множество: (s.inf' H f) при коэрцировании эквивалентно инф'_ по коэрцированным f.

LaTeX

$$@[simp, norm_cast] (instFunLike.coe (s.inf' H f)) = s.inf' H (λ i, instFunLike.coe (f i))$$

Lean4

@[simp, norm_cast]
theorem coe_inf' {ι : Type*} {s : Finset ι} (H : s.Nonempty) (f : ι → C(α, β)) :
    ⇑(s.inf' H f) = s.inf' H fun i ↦ ⇑(f i) := by ext; simp [inf'_apply]

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