PContinuous — Mathlib

English

A partial function f : X ⇀ Y is continuous if and only if the preimage of every open set in Y is open in X.

Русский

Частичное отображение f : X ⇀ Y непрерывно тогда и только тогда, когда предобраз любого открытого множества в Y является открытым в X.

LaTeX

$$$\\mathrm{PContinuous}(f) \\iff \\forall S, \\mathrm{IsOpen}(S) \\to \\mathrm{IsOpen}(f^{-1}(S))$$$

Lean4

/-- Continuity of a partial function -/
def PContinuous (f : X →. Y) :=
  ∀ s, IsOpen s → IsOpen (f.preimage s)

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