mem_univ_Ioc — Mathlib

English

An element x belongs to the product of all Ioc's over univ if and only if x ∈ I.

Русский

Элемент x принадлежит произведению всех Ioc на универсе тогда и только тогда, когда x ∈ I.

LaTeX

$$$$ (x ∈ \\pi \\text{univ} \\; \\text{fun } i \\mapsto Ioc (I.lower i) (I.upper i)) \\iff x \\in I $$$$

Lean4

theorem mem_univ_Ioc {I : Box ι} : (x ∈ pi univ fun i ↦ Ioc (I.lower i) (I.upper i)) ↔ x ∈ I :=
  mem_univ_pi

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