pi_inf_principal_pi_eq_bot — Mathlib

English

A refined form of pi_inf_principal_univ_pi_eq_bot for arbitrary I with i ∈ I when taking bottom.

Русский

Уточнение для произвольного I по отношению к нижнему элементу.

LaTeX

$$$\pi f \inf \mathfrak{P}(\mathrm{Set.pi}(I, s)) = \bot \iff \exists i \in I, f_i \inf \mathfrak{P}(s_i) = \bot$$$

Lean4

@[simp]
theorem pi_inf_principal_pi_eq_bot [∀ i, NeBot (f i)] {I : Set ι} :
    pi f ⊓ 𝓟 (Set.pi I s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥ := by
  classical
  rw [← univ_pi_piecewise_univ I, pi_inf_principal_univ_pi_eq_bot]
  refine exists_congr fun i => ?_
  by_cases hi : i ∈ I <;> simp [hi, NeBot.ne']

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