image_infs — Mathlib

English

Applying a structure-preserving map commutes with infimum: map_f(s ⊼ t) = map_f(s) ⊼ map_f(t).

Русский

Применение отображения, сохраняющего структуру, сохраняет инф: map_f(s ⊼ t) = map_f(s) ⊼ map_f(t).

LaTeX

$$$ \operatorname{map}_f (s \⊼ t) = (\operatorname{map}_f s) \⊼ (\operatorname{map}_f t) $$$

Lean4

theorem image_infs (f : F) (s t : Finset α) : image f (s ⊼ t) = image f s ⊼ image f t :=
  image_image₂_distrib <| map_inf f

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