implicitToOpenPartialHomeomorphOfComplemented

English

Two successive compositions satisfy associativity: (p.compContinuousLinearMap u1).compContinuousLinearMap u2 = p.compContinuousLinearMap (u1.comp u2).

Русский

Двойная композиция линейных отображений ассоциативна: (p.compContinuousLinearMap u1).compContinuousLinearMap u2 = p.compContinuousLinearMap (u1.comp u2).

LaTeX

$$(p.compContinuousLinearMap u1).compContinuousLinearMap u2 = p.compContinuousLinearMap (u1.comp u2)$$

Lean4

/-- An open partial homeomorphism between `E` and `F × f'.ker` sending level surfaces of `f`
to vertical subspaces. -/
def implicitToOpenPartialHomeomorphOfComplemented (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤)
    (hker : (ker f').ClosedComplemented) : OpenPartialHomeomorph E (F × ker f') :=
  (implicitFunctionDataOfComplemented f f' hf hf' hker).toOpenPartialHomeomorph

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