instDilationClassOfDilationEquivClass

English

If F carries an EquivLike structure from X to Y and there is a DilationEquivClass on F, then F forms a DilationClass between X and Y.

Русский

Если F имеет структуру эквивалиентичного отображения между X и Y и существует класс дилатаций DilationEquivClass для F, то F образует дилатационный класс между X и Y.

LaTeX

$$$\forall F X Y,\ [\text{EquivLike } F X Y]\ [\text{DilationEquivClass } F X Y] \Rightarrow \text{DilationClass } F X Y$$$

Lean4

instance (priority := 100) [EquivLike F X Y] [DilationEquivClass F X Y] : DilationClass F X Y :=
  { inferInstanceAs (FunLike F X Y), ‹DilationEquivClass F X Y› with }

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