iInf_apply — Mathlib

English

For a family of nuclei f: ι → Nucleus(X), the pointwise infimum iInf f is again a nucleus, and (iInf f) x = ⨅ i, f(i) x.

Русский

Для семейства нуклеусов f: ι → Nucleus(X) точечный инфимум iInf f является нуклеусом, и (iInf f) x = ⨅ i, f(i) x.

LaTeX

$$$ (\mathrm{iInf}\, f)\; x = \bigwedge_{i} f(i)(x) $$$

Lean4

@[simp]
theorem iInf_apply {ι : Type*} (f : ι → (Nucleus X)) (x : X) : iInf f x = ⨅ j, f j x := by
  rw [iInf, sInf_apply, iInf_range]

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