e_mem_of_eq_true — Mathlib

English

If x.val a = true, then e(...) a is a member of the corresponding factors list.

Русский

Если x.val a = true, то e(...) a является членом соответствующего списка факторов.

LaTeX

$$$\\forall {x : (π C (· ∈ s)) .Elem} {a : I}, (x.val a = true) \\Rightarrow e (π C (· ∈ s)) a \\in factors C s x$$$

Lean4

theorem e_mem_of_eq_true {x : (π C (· ∈ s))} {a : I} (hx : x.val a = true) : e (π C (· ∈ s)) a ∈ factors C s x :=
  by
  rcases x with ⟨_, z, hz, rfl⟩
  simp only [factors, List.mem_map, Finset.mem_sort]
  refine ⟨a, ?_, if_pos hx⟩
  aesop (add simp Proj)

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