Ico_eq_image_ssubsets — Mathlib

English

If s ⊆ t, then the interval Ico(s, t) is in bijection with unions s ∪ v where v runs over subsets of t \\ s; concretely Ico(s, t) = { s ∪ v : v ⊆ t \\ s }.

Русский

Если s ⊆ t, то интервал Ico(s, t) биекцию с объединением s и подмножеств t \\ s; то есть Ico(s, t) = { s ∪ v : v ⊆ t \\ s }.

LaTeX

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

Lean4

theorem Ico_eq_image_ssubsets (h : s ⊆ t) : Ico s t = (t \ s).ssubsets.image (s ∪ ·) :=
  by
  ext u
  simp_rw [mem_Ico, mem_image, mem_ssubsets]
  constructor
  · rintro ⟨hs, ht⟩
    exact ⟨u \ s, sdiff_lt_sdiff_right ht hs, sup_sdiff_cancel_right hs⟩
  · rintro ⟨v, hv, rfl⟩
    exact ⟨le_sup_left, sup_lt_of_lt_sdiff_left hv h⟩

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