C0 — Mathlib · SciLib

English

The subset C0 consists of those functions in C whose o-th coordinate is false.

Русский

Подмножество C0 состоит из функций из C, у которых на o-й координате значение равно false.

LaTeX

$$$ C0\; C\; ho = C \cap \{ f\;|\; f(\operatorname{term} I ho) = \text{false} \}$$$

Lean4

/-- The subset of `C` consisting of those elements whose `o`-th entry is `false`. -/
def C0 :=
  C ∩ {f | f (term I ho) = false}

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