isContained_congr — Mathlib

English

If A ≃g H and B ≃g G, then A ⊑ B iff H ⊑ G.

Русский

Если A ≃g H и B ≃g G, то A ⊑ B тогда же, когда H ⊑ G.

LaTeX

$$A \cong_g H ∧ B \cong_g G ⇒ (A ⊑ B ↔ H ⊑ G)$$

Lean4

/-- If `A ≃g H` and `B ≃g G` then `A` is contained in `B` if and only if `H` is contained
in `G`. -/
theorem isContained_congr (e₁ : A ≃g H) (e₂ : B ≃g G) : A ⊑ B ↔ H ⊑ G :=
  ⟨.trans' ⟨e₂.toCopy⟩ ∘ .trans ⟨e₁.symm.toCopy⟩, .trans' ⟨e₂.symm.toCopy⟩ ∘ .trans ⟨e₁.toCopy⟩⟩

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