image_subset_image

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.image_subset_image

English

For all R and t, a ∈ preimage R t iff ∃ b ∈ t with a ~[R] b.

Русский

Для всех R и t, a ∈ preimage R t тогда и только тогда, когда существует b ∈ t такое, что a ~[R] b.

LaTeX

$$a ∈ R.preimage\,t \iff ∃ b ∈ t, a ~[R] b$$

Lean4

@[gcongr]
theorem image_subset_image (hs : s₁ ⊆ s₂) : image R s₁ ⊆ image R s₂ := fun _ ⟨a, ha, hab⟩ ↦ ⟨a, hs ha, hab⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru