English
The inclusion pi s t1 ⊆ pi s t2 is equivalent to: for all i ∈ s, t1 i ⊆ t2 i, or pi s t1 = ∅.
Русский
Включение pi s t1 ⊆ pi s t2 эквивалентно: для всех i ∈ s, t1 i ⊆ t2 i, или pi s t1 пусто.
LaTeX
$$$$ \\ pi s t_1 \\subseteq \\ pi s t_2 \\iff \\Big( \\forall i \\in s,\\ t_1 i \\subseteq t_2 i \\Big) \\lor \\ pi s t_1 = \\emptyset. $$$$
Lean4
theorem pi_subset_pi_iff : pi s t₁ ⊆ pi s t₂ ↔ (∀ i ∈ s, t₁ i ⊆ t₂ i) ∨ pi s t₁ = ∅ :=
by
refine ⟨fun h => or_iff_not_imp_right.2 ?_, fun h => h.elim pi_mono fun h' => h'.symm ▸ empty_subset _⟩
rw [← Ne, ← nonempty_iff_ne_empty]
intro hne i hi
simpa only [eval_image_pi hi hne, eval_image_pi hi (hne.mono h)] using image_mono (f := fun f : ∀ i, α i => f i) h
