instMembershipForallReal — Mathlib

English

There is a canonical membership definition: x ∈ I iff ∀ i, x_i ∈ Ioc (I.lower_i) (I.upper_i).

Русский

Существует каноническое определение членства: x ∈ I тогда и только тогда, когда для каждого i выполняется x_i ∈ Ioc (I.lower_i) (I.upper_i).

LaTeX

$$$$x \\in I \\iff \\forall i, x_i \\in (I.lower i, I.upper i].$$$$

Lean4

instance : Membership (ι → ℝ) (Box ι) :=
  ⟨fun I x ↦ ∀ i, x i ∈ Ioc (I.lower i) (I.upper i)⟩

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