antitoneOn_of_rightInvOn_of_mapsTo

English

If φ is antitone on t, ψ is a right inverse of φ on s, and ψ maps s into t, then ψ is antitone on s.

Русский

Если φ антитонична на t, ψ является правым обратным к φ на s, и ψ отображает s в t, то ψ антитонична на s.

LaTeX

$$$\operatorname{AntitoneOn}(\varphi,t) \to \operatorname{RightInvOn}(\psi,\varphi,s) \to \operatorname{MapsTo}(\psi,s,t) \Rightarrow \operatorname{AntitoneOn}(\psi,s)$$$

Lean4

theorem antitoneOn_of_rightInvOn_of_mapsTo [PartialOrder α] [LinearOrder β] {φ : β → α} {ψ : α → β} {t : Set β}
    {s : Set α} (hφ : AntitoneOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : AntitoneOn ψ s :=
  (monotoneOn_of_rightInvOn_of_mapsTo hφ.dual_left φψs ψts).dual_right

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