preimage_iso — Mathlib

English

If φ is an order iso from α to β and t is a chain in β, then φ⁻¹'(t) is a chain in α.

Русский

Если φ — порядок-изоморфизм α к β и t — цепь в β, то φ⁻¹'(t) — цепь в α.

LaTeX

$$$ IsChain\\ (≤)\\ t \\rightarrow IsChain\\ (≤)\\ (φ^{-1}' t) $$$

Lean4

theorem preimage_iso [LE α] [LE β] {t : Set β} (ht : IsChain (· ≤ ·) t) (φ : α ≃o β) : IsChain (· ≤ ·) (φ ⁻¹' t) :=
  preimage_relEmbedding ht _

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