IicFinsetSet — Mathlib

English

There is a canonical equivalence between the finite lower interval Iic(a) and the set {x ≤ a} in the ambient order.

Русский

Существует каноническое эквивалентное отображение между конечным нижним интервалом Iic(a) и множеством {x ≤ a} в пределах порядка.

LaTeX

$$Iic(a) \cong Set.Iic(a)$$

Lean4

/-- An equivalence between `Finset.Iic a` and `Set.Iic a`. -/
def _root_.Equiv.IicFinsetSet (a : α) : Iic a ≃ Set.Iic a
    where
  toFun b := ⟨b.1, coe_Iic a ▸ mem_coe.2 b.2⟩
  invFun b := ⟨b.1, by rw [← mem_coe, coe_Iic a]; exact b.2⟩

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