biUnion_image_inf_left — Mathlib

English

The left biUnion with images distributes to inf: s.biUnion (a ↦ t.image (a ∧ ·)) = s ⊼ t.

Русский

Левое биобъединение с образами распределяется на инфимума: s.biUnion (a ↦ t.image (a ∧ ·)) = s ⊼ t.

LaTeX

$$$ s.\text{biUnion}(\lambda a. t.\operatorname{image}(a \wedge \cdot)) = s \⊼ t $$$

Lean4

theorem biUnion_image_inf_left : s.biUnion (fun a ↦ t.image (a ⊓ ·)) = s ⊼ t :=
  biUnion_image_left

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