pi_mem_pi — Mathlib

English

If I is finite and all s_i belong to f_i for i ∈ I, then the cylinder I.pi s belongs to pi f.

Русский

Если I конечноe, и для каждого i ∈ I выполняется s_i ∈ f_i, тогда цилиндр I.pi s принадлежит pi f.

LaTeX

$$$I \text{ finite} \land (\forall i \in I, s_i \in f_i) \Rightarrow I.\pi s \in \pi f.$$$

Lean4

theorem pi_mem_pi {I : Set ι} (hI : I.Finite) (h : ∀ i ∈ I, s i ∈ f i) : I.pi s ∈ pi f :=
  by
  rw [pi_def, biInter_eq_iInter]
  refine mem_iInf_of_iInter hI (fun i => ?_) Subset.rfl
  exact preimage_mem_comap (h i i.2)

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