mem_iSup_prop — Mathlib

English

For any proposition p and family K : p → Subgroup G, the membership in the iSup over p of K is equivalent to either x equals the identity or there exists h with h ∈ p and x ∈ K(h).

Русский

Для любого предиката p и семейства K : p → Subgroup G принадлежность x к iSup над p эквивалентна либо x = e, либо существует h ∈ p, такое что x ∈ K(h).

LaTeX

$$$ x \\in \\iSup_{h: p} K h \\;\\iff\\; x = 1 \\;\\lor\\; \\exists h: p, x \\in K h $$$

Lean4

@[to_additive (attr := simp)]
theorem mem_iSup_prop {p : Prop} {K : p → Subgroup G} {x : G} : x ∈ ⨆ (h : p), K h ↔ x = 1 ∨ ∃ (h : p), x ∈ K h := by
  by_cases h : p <;> simp +contextual [h]

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