pi_mem_pi_iff — Mathlib

English

For a finite I, I.pi s ∈ pi f iff ∀ i ∈ I, s i ∈ f i (assuming NeBot).

Русский

Для конечного I: I.pi s ∈ pi f эквивалентно ∀ i ∈ I, s i ∈ f i (при условии NeBot).

LaTeX

$$[simp] theorem pi_mem_pi_iff ... : I.pi s ∈ pi f ↔ ∀ i ∈ I, s i ∈ f i$$

Lean4

@[simp]
theorem pi_mem_pi_iff [∀ i, NeBot (f i)] {I : Set ι} (hI : I.Finite) : I.pi s ∈ pi f ↔ ∀ i ∈ I, s i ∈ f i :=
  ⟨fun h _i hi => mem_of_pi_mem_pi h hi, pi_mem_pi hI⟩

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