isCofinalFor_fst_image_prod_snd_image

English

If s is directed under ≤, then the product of the images under fst and snd of s is cofinal in s.

Русский

Если s направлен относительно порядка ≤, то произведение образов под fst и snd от s будет кофинальным по отношению к s.

LaTeX

$$$$ \text{DirectedOn}(\le, s) \Rightarrow \mathrm{IsCofinalFor}\big((\mathrm{Prod.fst}'' s) \times \big(\mathrm{Prod.snd}'' s\big)\big) s. $$$$

Lean4

theorem isCofinalFor_fst_image_prod_snd_image {β : Type*} [Preorder β] {s : Set (α × β)} (hs : DirectedOn (· ≤ ·) s) :
    IsCofinalFor ((Prod.fst '' s) ×ˢ (Prod.snd '' s)) s :=
  by
  rintro ⟨_, _⟩ ⟨⟨x, hx, rfl⟩, y, hy, rfl⟩
  obtain ⟨z, hz, hxz, hyz⟩ := hs _ hx _ hy
  exact ⟨z, hz, hxz.1, hyz.2⟩

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