trans — Mathlib

English

A cofinal subset of a cofinal subset is cofinal.

Русский

Софинальное подмножество софинального подмножества кофайнально.

LaTeX

$${s t : Set α} (hs : IsCofinal s) (ht : IsCofinal t) : IsCofinal (Subtype.val '' t)$$

Lean4

/-- A cofinal subset of a cofinal subset is cofinal. -/
theorem trans {s : Set α} {t : Set s} (hs : IsCofinal s) (ht : IsCofinal t) : IsCofinal (Subtype.val '' t) :=
  by
  intro a
  obtain ⟨b, hb, hb'⟩ := hs a
  obtain ⟨c, hc, hc'⟩ := ht ⟨b, hb⟩
  exact ⟨c, Set.mem_image_of_mem _ hc, hb'.trans hc'⟩

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