Theorems · Definition · logic and foundations
FirstOrder.Language.Hom.range
{L : FirstOrder.Language} →
{M : Type w} → {N : Type u_1} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Hom M N → L.Substructure NThe range of a first-order hom f : M → N is a submodule of N.
See Note [range copy pattern].
- Defined in
- Mathlib.ModelTheory.Substructures
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Top.topproof · cited by 9,680
- Set.rangeproof · cited by 4,705
- FirstOrder.Languagestatement and proof · cited by 1,084
- FirstOrder.Language.Structurestatement and proof · cited by 775
- FirstOrder.Language.Substructurestatement · cited by 242
- FirstOrder.Language.Homstatement and proof · cited by 107
- FirstOrder.Language.Substructure.mapproof · cited by 49
- FirstOrder.Language.Substructure.copyproof · cited by 2
Cited by33
Results whose statement or proof uses this declaration.
- FirstOrder.Language.Embedding.equivRangestatement and proof · cited by 14
- FirstOrder.Language.Hom.range_eq_mapstatement · cited by 7
- FirstOrder.Language.Structure.FG.rangestatement · cited by 7
- FirstOrder.Language.Embedding.toPartialEquivproof · cited by 6
- FirstOrder.Language.Substructure.range_subtypestatement · cited by 3
- FirstOrder.Language.Embedding.subtype_equivRangestatement and proof · cited by 2
- FirstOrder.Language.Hom.map_le_rangestatement and proof · cited by 2
- FirstOrder.Language.Hom.range_eq_topstatement · cited by 2
- FirstOrder.Language.age.jointEmbeddingproof · cited by 2
- FirstOrder.Language.IsUltrahomogeneous.extend_embeddingproof · cited by 2
- FirstOrder.Language.PartialEquiv.domRestrictproof · cited by 2