preimage_iso_iff — Mathlib

English

IsChain r on φ⁻¹'(t) is equivalent to IsChain r' on t when φ is an order iso.

Русский

IsChain r на φ⁻¹'(t) эквивалентно IsChain r' на t, когда φ — OrderIso.

LaTeX

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

Lean4

theorem preimage_iso_iff [LE α] [LE β] {t : Set β} {φ : α ≃o β} : IsChain (· ≤ ·) (φ ⁻¹' t) ↔ IsChain (· ≤ ·) t :=
  ⟨fun h => (φ.image_preimage t).subst (h.image_iso φ), fun h => h.preimage_iso _⟩

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