iInf_extend_top — Mathlib

English

Let e: I → J be injective and f: I → α. Then the infimum over j of (extend e f)(⊤) evaluated at j equals the infimum of f over I; i.e. ∧_{j} (extend e f)(⊤)(j) = ∧_{i} f(i).

Русский

Пусть e : I → J — инъекция и f : I → α. Тогда inf_{j} ((extend e f)(⊤))(j) равен inf_{i} f(i).

LaTeX

$$$$ \bigwedge_j (\operatorname{extend}(e,f)(\top))(j) = \bigwedge_i f(i) $$$$

Lean4

theorem iInf_extend_top {e : ι → β} (he : Injective e) (f : ι → α) : ⨅ j, extend e f ⊤ j = iInf f :=
  @iSup_extend_bot αᵒᵈ _ _ _ _ he _

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