lowerClosure_image — Mathlib

English

LowerClosure respects order-isomorphism: lowerClosure (f''s) = LowerSet.map f (lowerClosure s).

Русский

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

LaTeX

$$$lowerClosure (f''s) = LowerSet.map f (lowerClosure s)$$$

Lean4

@[simp]
theorem lowerClosure_image (f : α ≃o β) : lowerClosure (f '' s) = LowerSet.map f (lowerClosure s) :=
  by
  rw [← f.symm_symm, ← LowerSet.symm_map, f.symm_symm]
  ext
  simp [-LowerSet.symm_map, LowerSet.map, OrderIso.symm, ← f.symm_apply_le]

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