setSeq_prod_subset — Mathlib

English

If N ≤ m and N ≤ n, then setSeq(m) × setSeq(n) ⊆ U(N).

Русский

Если N ≤ m и N ≤ n, тогда setSeq(m) × setSeq(n) ⊆ U(N).

LaTeX

$$$(\text{setSeq}(hf,U_{mem},m) \timesˢ \text{setSeq}(hf,U_{mem},n)) \subseteq U(N)$$$

Lean4

theorem setSeq_prod_subset {N m n} (hm : N ≤ m) (hn : N ≤ n) : setSeq hf U_mem m ×ˢ setSeq hf U_mem n ⊆ U N :=
  fun p hp => by
  refine (setSeqAux hf U_mem N).2.2 ⟨?_, ?_⟩ <;> apply setSeq_sub_aux
  · exact setSeq_mono hf U_mem hm hp.1
  · exact setSeq_mono hf U_mem hn hp.2

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