map_iInf — Mathlib

English

If f is injective, map distributes over arbitrary infimum: (iInf s).map f = ⨅ i, (s i).map f.

Русский

Если f инъективен, отображение распределяется по произвольному инфимину: (iInf s).map f = ⨅ i, (s i).map f.

LaTeX

$$$\big(\mathrm{iInf}\,s\big).map f = \big(\inf_i (s(i).map f)\big) \quad \text{if } f \text{ injective}$$$

Lean4

@[to_additive]
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : F) (hf : Function.Injective f) (s : ι → Submonoid M) :
    (iInf s).map f = ⨅ i, (s i).map f := by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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