subset_coe_map — Mathlib

English

If f is an order-preserving map, then for any interval s the image f''s is contained in the interval s.map f.

Русский

Если f — отображение, сохраняющее порядок, то изображение интервала s лежит внутри интервала, полученного применением f к s.

LaTeX

$$$$ \\forall f:\\alpha \\to_{?} \\beta, \\forall s \\in Interval(\\alpha): f '' s \\subseteq s.map\: f. $$$$

Lean4

theorem subset_coe_map (f : α →o β) : ∀ s : Interval α, f '' s ⊆ s.map f
  | ⊥ => by simp
  | (s : NonemptyInterval α) => s.subset_coe_map _

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