iInf_subtype — Mathlib

English

Let p be a predicate on ι and f : Subtype p → α. Then the infimum of f equals the infimum over i of f restricted to i with witness h: p i.

Русский

Пусть p — предикат на ι и f : Subtype p → α. Тогда ⨅ f = ⨅_{i} ⨅_{h : p i} f⟨i,h⟩.

LaTeX

$$$$\bigwedge_{x : Subtype p} f(x) = \bigwedge_{i} \bigwedge_{h : p i} f(i,h).$$$$

Lean4

theorem iInf_subtype : ∀ {p : ι → Prop} {f : Subtype p → α}, iInf f = ⨅ (i) (h : p i), f ⟨i, h⟩ :=
  @iSup_subtype αᵒᵈ _ _

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