LEComap — Mathlib

English

Given a continuous map f: X → Y, LEComap f A B expresses that A refines the pullback of B along f.

Русский

Для непрерывного отображения f: X → Y LEComap f A B выражает, что A рефинементно отображается в B через f.

LaTeX

$$$$\\mathrm{LEComap}(f, A, B) \\iff A \\le B.\\mathrm{comap}(f).$$$$

Lean4

/-- Given `f : C(X, Y)`, `DiscreteQuotient.LEComap f A B` is defined as
`A ≤ B.comap f`. Mathematically this means that `f` descends to a morphism `A → B`. -/
def LEComap : Prop :=
  A ≤ B.comap f

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