mem_cylinder

Mathlib.MeasureTheory.Constructions.Cylinders

URI: https://scilib.ai/kg/mathlib#MeasureTheory.mem_cylinder

English

A function f lies in cylinder(s,S) if and only if its restriction to s lies in S.

Русский

Элемент f лежит в цилиндре, если и только если ограничение f на s принадлежит S.

LaTeX

$$$$f \\in \\mathrm{cylinder}(s,S) \\iff s.restrict(f) \\in S.$$$$

Lean4

@[simp]
theorem mem_cylinder (s : Finset ι) (S : Set (∀ i : s, α i)) (f : ∀ i, α i) : f ∈ cylinder s S ↔ s.restrict f ∈ S :=
  mem_preimage

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

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

Разделы

Аффилиация

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