mem_of_pi_mem_pi — Mathlib

English

If I.pi s ∈ pi f, then for any i ∈ I, s i ∈ f i.

Русский

Если I.pi s принадлежит pi f, то для любого i ∈ I выполняется s i ∈ f i.

LaTeX

$$$I \text{ pi } s \in \pi f \Rightarrow \forall i \in I, s i \in f i$$$

Lean4

theorem mem_of_pi_mem_pi [∀ i, NeBot (f i)] {I : Set ι} (h : I.pi s ∈ pi f) {i : ι} (hi : i ∈ I) : s i ∈ f i := by
  classical
  rcases mem_pi.1 h with ⟨I', -, t, htf, hts⟩
  refine mem_of_superset (htf i) fun x hx => ?_
  have : ∀ i, (t i).Nonempty := fun i => nonempty_of_mem (htf i)
  choose g hg using this
  have : update g i x ∈ I'.pi t := fun j _ => by rcases eq_or_ne j i with (rfl | hne) <;> simp [*]
  simpa using hts this i hi

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