one_sub_e_mem_of_false — Mathlib

English

If y.val a = true and x.val a = false, then 1 − e(π C (· ∈ s)) a is in factors C s x.

Русский

Если y.val a = true и x.val a = false, то 1 − e(π C (· ∈ s)) a принадлежит factors C s x.

LaTeX

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

Lean4

theorem one_sub_e_mem_of_false {x y : (π C (· ∈ s))} {a : I} (ha : y.val a = true) (hx : x.val a = false) :
    1 - e (π C (· ∈ s)) a ∈ factors C s x :=
  by
  simp only [factors, List.mem_map, Finset.mem_sort]
  use a
  simp only [hx]
  rcases y with ⟨_, z, hz, rfl⟩
  aesop (add simp Proj)

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