map_infs — Mathlib

English

The image of infimum equals infimum of images: image f (s ⊼ t) = image f s ⊼ image f t.

Русский

Образ инфимума равен инфимууму образов: image f (s ⊼ t) = image f s ⊼ image f t.

LaTeX

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

Lean4

theorem map_infs (f : F) (hf) (s t : Finset α) : map ⟨f, hf⟩ (s ⊼ t) = map ⟨f, hf⟩ s ⊼ map ⟨f, hf⟩ t := by
  simpa [map_eq_image] using image_infs f s t

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