instMulZeroOneClass — Mathlib

English

If Y has MulZeroOneClass, then LocallyConstant(X,Y) has MulZeroOneClass, with both 0 and 1 defined pointwise.

Русский

Если у Y есть MulZeroOneClass, то LocallyConstant(X,Y) имеет MulZeroOneClass, с нулём и единицей, определёнными по месту.

LaTeX

$$LocallyConstant(X,Y) has a MulZeroOneClass structure (pointwise).$$

Lean4

instance [MulZeroOneClass Y] : MulZeroOneClass (LocallyConstant X Y) :=
  Function.Injective.mulZeroOneClass DFunLike.coe DFunLike.coe_injective' rfl rfl fun _ _ => rfl

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