image_of_monotone — Mathlib

English

If s ⊆ α is cofinal in t ⊆ α and f is monotone, then the image of s under f is cofinal in the image of t under f.

Русский

Пусть s зачало кофинально по отношению к t, и f монотонная: тогда образ s под действием f является кофинальным по отношению к образу t.

LaTeX

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

Lean4

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

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