Icc_eq_image_powerset — Mathlib

English

If s ⊆ t, then the closed interval Icc(s, t) is in bijection with subsets of t \\ s via the map v ↦ s ∪ v; equivalently Icc(s, t) = { s ∪ v : v ⊆ t \\ s }.

Русский

Если s ⊆ t, то замкнутый интервал Icc(s, t) задаётся биекцией с подмножествами t \\ s посредством отображения v ↦ s ∪ v; то есть Icc(s, t) = { s ∪ v : v ⊆ t \\ s }.

LaTeX

$$$Icc(s,t) = \\{ s \\cup v \\mid v \\subseteq t \\setminus s \\}$$$

Lean4

theorem Icc_eq_image_powerset (h : s ⊆ t) : Icc s t = (t \ s).powerset.image (s ∪ ·) :=
  by
  unfold Finset.Icc instLocallyFiniteOrder LocallyFiniteOrder.ofIcc
  ext
  simp [h, union_comm]

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