forall_disjSups_iff — Mathlib

English

The disjSups of a right-hand union distributes over union: s ○ (t₁ ∪ t₂) = s ○ t₁ ∪ s ○ t₂.

Русский

ДисjointSups справа по объединению распределяется: s ○ (t₁ ∪ t₂) = s ○ t₁ ∪ s ○ t₂.

LaTeX

$$$ s \circ (t_{1} \cup t_{2}) = s \circ t_{1} \cup s \circ t_{2} $$$

Lean4

theorem forall_disjSups_iff {p : α → Prop} : (∀ c ∈ s ○ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b) :=
  by
  simp_rw [mem_disjSups]
  refine ⟨fun h a ha b hb hab => h _ ⟨_, ha, _, hb, hab, rfl⟩, ?_⟩
  rintro h _ ⟨a, ha, b, hb, hab, rfl⟩
  exact h _ ha _ hb hab

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