dom_of_le_some — Mathlib

English

Let x be an element of PartENat and y a natural number. If x is bounded above by the finite element corresponding to y, i.e. x ≤ some y (cast to PartENat), then x has a representation in the domain (i.e. x is finite).

Русский

Пусть x ∈ PartENat и y ∈ ℕ. Если x ограничено сверху конечным элементом, соответствующим y, то x принадлежит области определения (то есть является конечным элементом).

LaTeX

$$$ x \le \hat{y} \Rightarrow \mathrm{Dom}(x) $$$

Lean4

theorem dom_of_le_some {x : PartENat} {y : ℕ} (h : x ≤ some y) : x.Dom :=
  dom_of_le_of_dom h trivial

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