mem_pi_of_mem

Mathlib.Order.Filter.Pi

URI: https://scilib.ai/kg/mathlib#Filter.mem_pi_of_mem

English

If s ∈ f i, then preimage of s under eval i belongs to pi f.

Русский

Если s ∈ f_i, то прообраз под eval_i принадлежит pi f.

LaTeX

$$$\text{If } s \in f_i, \text{ then } \mathrm{eval}_i^{-1}(s) \in \pi f.$$$

Lean4

theorem mem_pi_of_mem (i : ι) {s : Set (α i)} (hs : s ∈ f i) : eval i ⁻¹' s ∈ pi f :=
  mem_iInf_of_mem i <| preimage_mem_comap hs

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru