upperClosure_image — Mathlib

English

UpperClosure respects order-isomorphism: upperClosure (f''s) = UpperSet.map f (upperClosure s).

Русский

UpperClosure сохраняет изображение через ордер-изоморфизм: upperClosure (f''s) = UpperSet.map f (upperClosure s).

LaTeX

$$$upperClosure (f''s) = UpperSet.map f (upperClosure s)$$$

Lean4

@[simp]
theorem upperClosure_image (f : α ≃o β) : upperClosure (f '' s) = UpperSet.map f (upperClosure s) :=
  by
  rw [← f.symm_symm, ← UpperSet.symm_map, f.symm_symm]
  ext
  simp [-UpperSet.symm_map, UpperSet.map, OrderIso.symm, ← f.le_symm_apply]

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