pi_def — Mathlib

English

Let i be a set of α and s a family of sets indexed by α, the pi-type construction expresses as an intersection over a ∈ i of eval a preimage of s a.

Русский

Пусть i ⊆ α, и пусть s(a) — множество, тогда pi i s = ⋂_{a ∈ i} eval(a)^{-1}(s(a)).

LaTeX

$$$$ \pi i s = \bigcap_{a \in i} \operatorname{eval}_a^{-1}(s(a)) $$$$

Lean4

theorem pi_def (i : Set α) (s : ∀ a, Set (π a)) : pi i s = ⋂ a ∈ i, eval a ⁻¹' s a :=
  by
  ext
  simp

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