univ_pi_subset_univ_pi_iff — Mathlib

English

The implication pi univ t1 ⊆ pi univ t2 is equivalent to: for all i, t1 i ⊆ t2 i or there exists i with t1 i = ∅.

Русский

Пусть pi univ t1 ⊆ pi univ t2 тогда и только тогда, когда для каждого i выполняется t1 i ⊆ t2 i или существует i с t1 i = ∅.

LaTeX

$$$$ \\pi\\mathrm{univ}\\ t_1 \\subseteq \\pi\\mathrm{univ}\\ t_2 \\iff (\\forall i, t_1 i \\subseteq t_2 i) \\lor \\exists i, t_1 i = \\emptyset. $$$$

Lean4

theorem univ_pi_subset_univ_pi_iff : pi univ t₁ ⊆ pi univ t₂ ↔ (∀ i, t₁ i ⊆ t₂ i) ∨ ∃ i, t₁ i = ∅ := by
  simp [pi_subset_pi_iff]

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