le_domain_toRationalMap — Mathlib

English

For any partial map f: X.PartialMap Y, its domain is contained in the domain of its associated rational map.

Русский

Для любой частичной карты f: X.PartialMap Y область определения включена в область Определения соответствующей рациональной карты.

LaTeX

$$$f.domain \le f.toRationalMap.domain$$$

Lean4

theorem le_domain_toRationalMap (f : X.PartialMap Y) : f.domain ≤ f.toRationalMap.domain :=
  le_sSup ⟨f, rfl, rfl⟩

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