mem_balancedCore_iff — Mathlib

English

Simplified equivalences for membership in balancedCore via nested conjunctions.

Русский

Упрощённые эквивалентности принадлежности в balancedCore через вложенные конъюнкции.

LaTeX

$$$x \\in balancedCore 𝕜 s \\iff \\exists t, Balanced 𝕜 t \\land t \\subseteq s \\land x \\in t$$$

Lean4

theorem mem_balancedCore_iff : x ∈ balancedCore 𝕜 s ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t := by
  simp_rw [balancedCore, mem_sUnion, mem_setOf_eq, and_assoc]

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