image_of_antitone — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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