isBounded_image_fst_and_snd — Mathlib

English

A subset s ⊆ α×β is bounded iff both its projections on α and β are bounded.

Русский

Подмножество s ⊆ α×β ограничено тогда и только тогда, когда обе проекции на α и на β ограничены.

LaTeX

$$$\operatorname{IsBounded}(\operatorname{Prod.fst}''s) \\land \\operatorname{IsBounded}(\operatorname{Prod.snd}''s) \,\iff \, \operatorname{IsBounded}(s)$$$

Lean4

theorem isBounded_image_fst_and_snd {s : Set (α × β)} :
    IsBounded (Prod.fst '' s) ∧ IsBounded (Prod.snd '' s) ↔ IsBounded s :=
  compl_mem_coprod.symm

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