uniqueElim_preimage — Mathlib

English

If ι has a unique element, then the preimage of the product pi univ t under uniqueElim is exactly t(default).

Русский

Пусть ι имеет единственный элемент; тогда прообраз подстановочного отображения uniqueElim от π-univ t равен t(значение по умолчанию).

LaTeX

$$$ \mathrm{uniqueElim}^{-1}(\pi \mathrm{univ}\ t) = t(\mathrm{default}) $$$

Lean4

theorem uniqueElim_preimage [Unique ι] (t : ∀ i, Set (α i)) : uniqueElim ⁻¹' pi univ t = t (default : ι) := by ext;
  simp [Unique.forall_iff]

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