supIrredLowerSet_apply — Mathlib

English

For a finite α, the inverse of supIrredLowerSet on a sup-irreducible lower set s is the join of the elements of s; more precisely, supIrredLowerSet.symm s = (s.1 : Set α).toFinset.sup id.

Русский

Для конечного α обратное отображение supIrredLowerSet на суп-irreducible нижнее множество s равно объединению элементов s, то есть supIrredLowerSet.symm s = (s.1 : Set α).toFinset.sup id.

LaTeX

$$$ (\\mathrm{supIrredLowerSet})^{-1}(s) = \\bigvee_{a \\in s.1} a$$$

Lean4

@[simp]
theorem supIrredLowerSet_apply (a : α) : supIrredLowerSet a = ⟨Iic a, supIrred_Iic _⟩ :=
  rfl

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