leftInverse_of_card_le — Mathlib

English

If f: α → β has a right inverse g and card β ≤ card α, then g is a left inverse of f.

Русский

Если существует правая обратная g к f и card β ≤ card α, то g является левой обратной к f.

LaTeX

$$$\\text{RightInverse } f g \\land \\operatorname{card} \\beta \\le \\operatorname{card} \\alpha \\Rightarrow \\text{LeftInverse } f g$$$

Lean4

theorem _root_.Function.RightInverse.leftInverse_of_card_le {f : α → β} {g : β → α} (hfg : RightInverse f g)
    (hcard : card β ≤ card α) : LeftInverse f g :=
  Function.LeftInverse.rightInverse_of_card_le hfg hcard

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