pi — Mathlib · SciLib

English

For sets s,t, s ×ˢ t equals fst^{-1}(s) ∩ snd^{-1}(t).

Русский

Для множеств s,t верно s ×ˢ t = fst^{-1}(s) ∩ snd^{-1}(t).

LaTeX

$$$$s \\timesˢ t = \\mathrm{fst}^{-1}(s) \\cap \\mathrm{snd}^{-1}(t).$$$$

Lean4

/-- Given an index set `ι` and a family of sets `t : Π i, Set (α i)`, `pi s t`
is the set of dependent functions `f : Πa, π a` such that `f i` belongs to `t i`
whenever `i ∈ s`. -/
def pi (s : Set ι) (t : ∀ i, Set (α i)) : Set (∀ i, α i) :=
  {f | ∀ i ∈ s, f i ∈ t i}

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