image_of_antitone — Mathlib

English

If scofinal and f is antitone, then the image of s under f is cofinal in the image of t under f.

Русский

Пусть s кофинальное в t и f антинтонична; тогда образ s по f кофинален в образе t по f.

LaTeX

$$$ \\IsCofinalFor\\ s\\ t \\rightarrow \\operatorname{Antitone} f \\rightarrow \\IsCofinalFor(\\mathrm{image} f\\ s)(\\mathrm{image} f\\ t) $$$

Lean4

theorem image_of_antitone (hst : IsCofinalFor s t) (hf : Antitone f) : IsCoinitialFor (f '' s) (f '' t) :=
  by
  simp only [IsCoinitialFor, forall_mem_image, exists_mem_image]
  rintro a ha
  obtain ⟨b, hb, hab⟩ := hst ha
  exact ⟨b, hb, hf hab⟩

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