English
If f : α <i β is a principal segment, then there is a natural order isomorphism between α and the open interval below f.top, given by a ↦ ⟨f a, f.lt_top a⟩ with the inverse given by extracting the first coordinate.
Русский
Если f : α <i β — главный сегмент, существует естественный порядок-изоморфизм между α и открытым интервалом ниже f.top, задаваемый a ↦ ⟨f a, f.lt_top a⟩, а обратное отображение извлекает первую координату.
LaTeX
$$$\\mathrm{orderIsoIio}(f):\\; \\alpha \\simeq_o \\mathrm{Iio}(f.top).$$$
Lean4
/-- If `f : α <i β` is a principal segment, this is the induced order
isomorphism `α ≃o Set.Iio f.top`. -/
@[simps! apply_coe]
noncomputable def orderIsoIio {α β : Type*} [PartialOrder α] [PartialOrder β] (f : α <i β) : α ≃o Set.Iio f.top
where
toEquiv :=
Equiv.ofBijective (f := fun a ↦ ⟨f a, f.lt_top a⟩)
(by
constructor
· intro x y hxy
exact f.injective (by simpa using hxy)
· rintro ⟨z, hz⟩
obtain ⟨x, hx⟩ := f.mem_range_of_rel_top hz
exact ⟨x, by simpa using hx⟩)
map_rel_iff' := by simp
