rel_iff — Mathlib

English

Let e be an embedding with IsRelIff. Then the relation on the ambient shape c' between e.f i1 and e.f i2 is equivalent to the relation on c between i1 and i2.

Русский

Пусть вложение e удовлетворяет условию IsRelIff. Тогда отношение c' между e.f(i1) и e.f(i2) эквивалентно отношению c между i1 и i2.

LaTeX

$$$ c'.Rel( e.f(i_1), e.f(i_2)) \\iff c.Rel(i_1,i_2) $$$

Lean4

theorem rel_iff [e.IsRelIff] (i₁ i₂ : ι) : c'.Rel (e.f i₁) (e.f i₂) ↔ c.Rel i₁ i₂ :=
  by
  constructor
  · apply IsRelIff.rel'
  · exact e.rel

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