image_of_monotone — Mathlib

English

If s ⊆ α is coinitial in t ⊆ α and f is monotone, then f''s is coinitial in f''t.

Русский

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

LaTeX

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

Lean4

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

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