boundary — Mathlib

English

The boundary of the N-dimensional unit cube I^N consists of those points y: N → I for which there exists an index i with y(i) = 0 or y(i) = 1.

Русский

Граница куба I^N состоит из функций y: N → I, у которых существует координата i, равная 0 или 1.

LaTeX

$$boundary(N) = { y: N → I : ∃ i, y(i) = 0 ∨ y(i) = 1 }$$

Lean4

/-- The points in a cube with at least one projection equal to 0 or 1. -/
def boundary (N : Type*) : Set (I^N) :=
  {y | ∃ i, y i = 0 ∨ y i = 1}

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