English
Stability under transfinite shape is invariant under order isomorphisms.
Русский
Стабильность по трансфинитной форме сохраняется под порядковыми изоморфизмами.
LaTeX
$$IsStableUnderTransfiniteCompositionOfShape_iff_of_orderIso$$
Lean4
theorem isStableUnderTransfiniteCompositionOfShape_iff_of_orderIso (e : J ≃o J') :
W.IsStableUnderTransfiniteCompositionOfShape J ↔ W.IsStableUnderTransfiniteCompositionOfShape J' := by
simp only [isStableUnderTransfiniteCompositionOfShape_iff, W.transfiniteCompositionsOfShape_eq_of_orderIso e]
