Evaluating an order isomorphism restricted to a principal down-set

OrderIso.Iic restricts an order isomorphism e : α ≃o β to the interval below a point, Set.Iic x ≃o Set.Iic (e x). It is built as a structure instance, so an application of it does not rewrite on its own: a consumer that meets (e.Iic x) y in a goal has to unfold the construction to get anywhere.

The two lemmas here supply the missing evaluation rules, in both directions. They hold by rfl, and stating them beside the construction rather than at any use site means no consumer needs the body of a composite order isomorphism exposed in order to compute with it.

@[simp]

theorem OrderIso.Iic_apply_coe {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (e : α ≃o β) (x : α) (y : ↑(Set.Iic x)) : ↑((e.Iic x) y) = e ↑y

Applying a restricted order isomorphism is applying the original.

@[simp]

theorem OrderIso.Iic_symm_apply_coe {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (e : α ≃o β) (x : α) (y : ↑(Set.Iic (e x))) : ↑((e.Iic x).symm y) = e.symm ↑y

Applying the inverse of a restricted order isomorphism is applying the original inverse.