mem_domain — Mathlib

English

An element x lies in the domain of a rational map f if and only if there exists a partial map g with x in its domain and g.toRationalMap = f.

Русский

Элемент x принадлежит области определения рациональной карты f тогда и только тогда, когда существует частичная карта g с x в области определения и g.toRationalMap = f.

LaTeX

$$$\forall f:X.RationalMap Y,\forall x,\ x\in f.domain \iff \exists g:X.PartialMap Y, x\in g.domain \land g.toRationalMap = f$$$

Lean4

theorem mem_domain {f : X ⤏ Y} {x} : x ∈ f.domain ↔ ∃ g : X.PartialMap Y, x ∈ g.domain ∧ g.toRationalMap = f :=
  TopologicalSpace.Opens.mem_sSup.trans (by simp [@and_comm (x ∈ _)])

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