English
There is an explicit description of the inverse of the isomorphism infIrredUpperSet: it sends an inf-irreducible upper set to the finite meet of its elements.
Русский
Существует явное описание обратного отображения для инф-нередуцируемого верхнего множества: образ обратного отображения InfIrredUpperSet — это конечная встреча элементов множества.
LaTeX
$$$ (\\operatorname{infIrredUpperSet})^{-1}(s) = \\bigwedge_{a \\in s.1} a$$$
Lean4
@[simp]
theorem infIrredUpperSet_symm_apply (s : { s : UpperSet α // InfIrred s }) [Fintype s] :
infIrredUpperSet.symm s = (s.1 : Set α).toFinset.inf id := by
classical
obtain ⟨s, hs⟩ := s
obtain ⟨a, rfl⟩ := infIrred_iff_of_finite.1 hs
cases nonempty_fintype α
have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder
simp [symm_apply_eq]
